Investigations into proof structures
From MaRDI portal
Cites work
- A finitely axiomatized formalization of predicate calculus with equality
- A legacy recalled and a tradition continued
- A Machine-Oriented Logic Based on the Resolution Principle
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- A simplified form of condensed detachment
- Asymptotic enumeration of compacted binary trees of bounded right height
- Automated reasoning contributes to mathematics and logic
- CODE: A powerful prover for problems of condensed detachment
- Condensed detachment as a rule of inference
- Conquering the Meredith single axiom
- Controlled integration of the cut rule into connection tableau calculi
- Efficient encodings of first-order Horn formulas in equational logic
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
- Evaluating general purpose automated theorem proving systems
- Faster, higher, stronger: E 2.3
- Final word on a shortest implicational axiom
- Finding shortest proofs: An application of linked inference rules
- From Schütte’s Formal Systems to Modern Automated Deduction
- Grammar-Based Tree Compression
- Handbook of automated reasoning. In 2 vols
- scientific article; zbMATH DE number 4209640 (Why is no real title available?)
- scientific article; zbMATH DE number 4063061 (Why is no real title available?)
- scientific article; zbMATH DE number 3774914 (Why is no real title available?)
- scientific article; zbMATH DE number 3782956 (Why is no real title available?)
- scientific article; zbMATH DE number 8327 (Why is no real title available?)
- scientific article; zbMATH DE number 48763 (Why is no real title available?)
- scientific article; zbMATH DE number 53302 (Why is no real title available?)
- scientific article; zbMATH DE number 177816 (Why is no real title available?)
- scientific article; zbMATH DE number 3568056 (Why is no real title available?)
- scientific article; zbMATH DE number 1348483 (Why is no real title available?)
- scientific article; zbMATH DE number 1042221 (Why is no real title available?)
- scientific article; zbMATH DE number 3303654 (Why is no real title available?)
- scientific article; zbMATH DE number 3335866 (Why is no real title available?)
- scientific article; zbMATH DE number 3200651 (Why is no real title available?)
- scientific article; zbMATH DE number 3045411 (Why is no real title available?)
- Hyper tableaux
- In memoriam Carew Arthur Meredith (1904-1976)
- Learning from Łukasiewicz and Meredith: investigations into proof structures
- Lemmas: generation, selection, application
- Machine learning guidance for connection tableaux
- Missing proofs found
- Notes on the axiomatics of the propositional calculus
- Principal type-schemes and condensed detachment
- Properties of substitutions and unifications
- Restricting backtracking in connection calculi
- SETHEO: A high-performance theorem prover
- Single axioms and axiom-pairs for the implicational fragments of \(\mathbf{R} \), R-Mingle, and some related systems
- SWI-Prolog
- The power of combining resonance with heat
- The resonance strategy
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Using hints to increase the effectiveness of an automated reasoning program: Case studies
- Variations on the Common Subexpression Problem
- Witness theory. Notes on -calculus and logic
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)
