Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
From MaRDI portal
Publication:331619
DOI10.1007/s10817-016-9367-3zbMath1402.03077OpenAlexW2324348649MaRDI QIDQ331619
Thierry Boy de la Tour, Nicolas Peltier
Publication date: 27 October 2016
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-016-9367-3
Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Combinatory logic and lambda calculus (03B40) Complexity of proofs (03F20)
Cites Work
- Unnamed Item
- Unnamed Item
- A typed \(\lambda\)-calculus for proving-by-example and bottom-up generalization procedure
- The epsilon calculus and Herbrand complexity
- The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem
- Generalizing proofs in monadic languages (with a postscript by Georg Kreisel).
- Proof theory. 2nd ed
- The number of proof lines and the size of proofs in first order logic
- A compact representation of proofs
- Unification under a mixed prefix
- Analogy in inductive theorem proving
- Theorem proving modulo
- A unification-theoretic method for investigating the \(k\)-provability problem
- Positive and negative results for higher-order disunification
- Proving theorems by reuse
- A Sequent Calculus with Implicit Term Representation
- Pruning the search space and extracting more models in tableaux
- A Tableaux Method for Systematic Simultaneous Search for Refutations and Models using Equational Problems
- Computer Science Logic
- Theorem Proving in Higher Order Logics
- A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
- Resolution in type theory
- Some Results on the Length of Proofs
This page was built for publication: Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
