Investigations into proof structures

DOI10.1007/S10817-024-09711-8MaRDI QIDQ6653096FDOQ6653096

Authors: Christoph Wernhard, Wolfgang Bibel 

Publication date: 16 December 2024

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

connection methodcondensed detachmentlemma generationanalysis of historic formal proofsautomated theorem proving in first-order logicproof structure terms

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Faster, higher, stronger: E 2.3
• SWI-Prolog
• CODE: A powerful prover for problems of condensed detachment
• Title not available (Why is that?)
• Variations on the Common Subexpression Problem
• Title not available (Why is that?)
• A Machine-Oriented Logic Based on the Resolution Principle
• Properties of substitutions and unifications
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• SETHEO: A high-performance theorem prover
• Evaluating general purpose automated theorem proving systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Handbook of automated reasoning. In 2 vols
• Grammar-Based Tree Compression
• Notes on the axiomatics of the propositional calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Using hints to increase the effectiveness of an automated reasoning program: Case studies
• Title not available (Why is that?)
• Title not available (Why is that?)
• Principal type-schemes and condensed detachment
• A finitely axiomatized formalization of predicate calculus with equality
• Automated reasoning contributes to mathematics and logic
• The resonance strategy
• A legacy recalled and a tradition continued
• Conquering the Meredith single axiom
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
• Hyper tableaux
• In memoriam Carew Arthur Meredith (1904-1976)
• Controlled integration of the cut rule into connection tableau calculi
• Title not available (Why is that?)
• Efficient encodings of first-order Horn formulas in equational logic
• Condensed detachment as a rule of inference
• The power of combining resonance with heat
• Asymptotic enumeration of compacted binary trees of bounded right height
• Title not available (Why is that?)
• Title not available (Why is that?)
• A simplified form of condensed detachment
• Machine learning guidance for connection tableaux
• Restricting backtracking in connection calculi
• Learning from Łukasiewicz and Meredith: investigations into proof structures
• Single Axioms and Axiom-Pairs for the Implicational Fragments of $$\mathbf {R}$$ R , R-Mingle, and Some Related Systems
• From Schütte’s Formal Systems to Modern Automated Deduction
• Finding shortest proofs: An application of linked inference rules
• Missing proofs found
• Final word on a shortest implicational axiom
• Title not available (Why is that?)
• Title not available (Why is that?)
• Lemmas: generation, selection, application

This page was built for publication: Investigations into proof structures

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