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

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

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)

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

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)