Introducing quantified cuts in logic with equality

DOI10.1007/978-3-319-08587-6_17zbMATH Open1423.68418arXiv1402.2474OpenAlexW1659517711MaRDI QIDQ3192194FDOQ3192194

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)

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.

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

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

Mathematics Subject Classification ID

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

Cited In (12)

• Title not available (Why is that?)
• Herbrand's theorem as higher order recursion
• On the cover complexity of finite languages
• Algorithmic introduction of quantified cuts
• Simulating non-prenex cuts in quantified propositional calculus
• On the Herbrand content of LK
• On the generation of quantified lemmas
• Title not available (Why is that?)
• Compressibility of Finite Languages by Grammars
• On the compressibility of finite languages and formal proofs
• System description: GAPT 2.0
• Inductive theorem proving based on tree 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)