Proof generalization in LK by second order unifier minimization

DOI10.1007/S10817-016-9367-3MaRDI QIDQ331619zbMATH OpenOpenAlexFDO

Authors 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

constraintsgeneralizationsecond-order unificationsequent calculus

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Complexity of proofs (03F20)

Recommendations

• The number of proof lines and the size of proofs in first order logic
• On the generation of quantified lemmas
• scientific article; zbMATH DE number 4135936
• Generalizing proofs in monadic languages (with a postscript by Georg Kreisel).
• scientific article; zbMATH DE number 1948175

Cites work

• A compact representation of proofs
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• A sequent calculus with implicit term representation
• A Tableaux Method for Systematic Simultaneous Search for Refutations and Models using Equational Problems
• A typed -calculus for proving-by-example and bottom-up generalization procedure
• A unification-theoretic method for investigating the \(k\)-provability problem
• Analogy in inductive theorem proving
• Computer Science Logic
• Generalizing proofs in monadic languages (with a postscript by Georg Kreisel).
• Higher-order unification and matching
• scientific article; zbMATH DE number 1765699 (Why is no real title available?)
• Positive and negative results for higher-order disunification
• Proof theory. 2nd ed
• Proving theorems by reuse
• Pruning the search space and extracting more models in tableaux
• Resolution in type theory
• Some Results on the Length of Proofs
• The epsilon calculus and Herbrand complexity
• The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem
• The number of proof lines and the size of proofs in first order logic
• Theorem Proving in Higher Order Logics
• Theorem proving modulo
• Unification under a mixed prefix

Cited in

(4)

• scientific article; zbMATH DE number 1948175 (Why is no real title available?)
• Unsound inferences make proofs shorter
• Second-order unification in the presence of linear shallow algebraic equations
• Title not available (Why is no real title available?)

This page was built for publication: Proof generalization in \(\mathrm {LK}\) by second order unifier minimization

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q331619)