Proof generalization in \(\mathrm {LK}\) by second order unifier minimization

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

zbMATH Keywords

sequent calculusgeneralizationconstraintssecond-order unification

Mathematics Subject Classification ID

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