Introducing quantified cuts in logic with equality

DOI10.1007/978-3-319-08587-6_17MaRDI QIDQ3192194zbMATH OpenOpenAlexFDO

Authors Stefan Hetzl, Alexander Leitsch, Giselle Reis, Janos Tapolczai, Daniel Weller

Publication date 26 September 2014

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1402.2474

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Mechanization of proofs and logical operations (03B35)

Abstract: Cut-introduction is a technique for structuring and compressing formal proofs. In this paper we generalize our cut-introduction method for the introduction of quantified lemmas of the form $forallx.A$ (for quantifier-free $A$) to a method generating lemmas of the form $forall{x}_{1}ldotsforall{x}_n.A$. Moreover, we extend the original method to predicate logic with equality. The new method was implemented and applied to the TSTP proof database. It is shown that the extension of the method to handle equality and quantifier-blocks leads to a substantial improvement of the old algorithm.

Recommendations

• On the generation of quantified lemmas
• Algorithmic introduction of quantified cuts
• Towards Algorithmic Cut-Introduction
• Atomic cut introduction by resolution: proof structuring and compression
• scientific article; zbMATH DE number 1088197

Cited in

(12)

• Inductive theorem proving based on tree grammars
• Herbrand's theorem as higher order recursion
• scientific article; zbMATH DE number 7447752 (Why is no real title available?)
• Algorithmic introduction of quantified cuts
• On the cover complexity of finite languages
• Simulating non-prenex cuts in quantified propositional calculus
• On the Herbrand content of LK
• On the generation of quantified lemmas
• scientific article; zbMATH DE number 1961528 (Why is no real title available?)
• Compressibility of Finite Languages by Grammars
• On the compressibility of finite languages and formal proofs
• System description: GAPT 2.0

This page was built for publication: Introducing quantified cuts in logic with equality

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