The Kreisel length-of-proof problem
type: Item
instance of: scholarly article
title: The Kreisel length-of-proof problem
zbMATH Open document ID: 0865.03044
DOI: 10.1007/BF01531022
author: William M. Farmer
published in: Annals of Mathematics and Artificial Intelligence
publication date: 1997-05-13T00:00:00Z
Mathematics Subject Classification ID: 03F20
zbMATH DE Number: 1005820
zbMATH Keywords: first-order system
zbMATH Keywords: Kreisel length-of-proof property
zbMATH Keywords: Parikh system
zbMATH Keywords: Peano arithmetic
zbMATH Keywords: unification
MaRDI profile type: Publication
cites work: Q4052071
cites work: A unification algorithm for second-order monadic terms
cites work: Simple second-order languages for which unification is undecidable
cites work: A unification-theoretic method for investigating the \(k\)-provability problem
cites work: One hundred and two problems in mathematical logic
cites work: The undecidability of the second-order unification problem
cites work: Q5812175
cites work: Unification: a multidisciplinary survey
cites work: Q3786479
cites work: The number of proof lines and the size of proofs in first order logic
cites work: On the length of proofs in formal systems
cites work: Q4124795
cites work: Some Results on the Length of Proofs
cites work: Q3815293
cites work: Sets of theorems with short proofs
cites work: Unification theory
cites work: A simplified formalization of predicate logic with identity
cites work: A theorem on the formalized arithmetic with function symbols ' and +
cites work: A note on a formalized arithmetic with function symbols ' and +
cites work: Taking out LK parts from a proof in Peano arithmetic
description: scientific article; zbMATH DE number 1005820