Pages that link to "Item:Q1102280"
From MaRDI portal
The following pages link to The number of proof lines and the size of proofs in first order logic (Q1102280):
Displayed 32 items.
- Proof generalization in \(\mathrm {LK}\) by second order unifier minimization (Q331619) (← links)
- Interpolants, cut elimination and flow graphs for the propositional calculus (Q674415) (← links)
- Regular expression order-sorted unification and matching (Q741252) (← links)
- The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem (Q843609) (← links)
- Generalizing proofs in monadic languages (with a postscript by Georg Kreisel). (Q930260) (← links)
- On the number of steps in proofs (Q1119576) (← links)
- The undecidability of \(k\)-provability (Q1176199) (← links)
- Bounded arithmetic, proof complexity and two papers of Parikh (Q1295443) (← links)
- Depth of proofs, depth of cut-formulas and complexity of cut formulas (Q1329747) (← links)
- The Kreisel length-of-proof problem (Q1353977) (← links)
- On the compressibility of finite languages and formal proofs (Q1706152) (← links)
- A unification-theoretic method for investigating the \(k\)-provability problem (Q1814133) (← links)
- Generalizing theorems in real closed fields (Q1899140) (← links)
- Refinement of bounds of the height of terms in the most general unifier (Q1977922) (← links)
- \(k\)-provability in \(\mathrm{PA}\) (Q2070428) (← links)
- The number of axioms (Q2120967) (← links)
- The undecidability of proof search when equality is a logical connective (Q2134939) (← links)
- Essential structure of proofs as a measure of complexity (Q2183713) (← links)
- Cut-elimination: syntax and semantics (Q2259012) (← links)
- Proof schemata in Hilbert-type axiomatic theories (Q2276941) (← links)
- Herbrand's theorem and term induction (Q2491080) (← links)
- Controlling witnesses (Q2566063) (← links)
- Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\) (Q2577589) (← links)
- A theorem on generalizations of proofs (Q2640597) (← links)
- On the non-confluence of cut-elimination (Q3083141) (← links)
- Note on the Benefit of Proof Representations by Name (Q3305625) (← links)
- Kreisel's Conjecture with minimality principle (Q3399187) (← links)
- 1994–1995 Winter Meeting of the Association for Symbolic Logic (Q4858810) (← links)
- Informational logic for automated reasoning (Q5236445) (← links)
- A Tableaux-Based Decision Procedure for Multi-parameter Propositional Schemata (Q5495914) (← links)
- Asymptotic cyclic expansion and bridge groups of formal proofs (Q5945614) (← links)
- Herbrand complexity and the epsilon calculus with equality (Q6178471) (← links)