Condensed detachment as a rule of inference

DOI10.1007/BF01371632zbMath0568.03010WikidataQ29541784 ScholiaQ29541784MaRDI QIDQ1060210

John A. Kalman

Publication date: 1983

Published in: Studia Logica (Search for Journal in Brave)

zbMATH Keywords

resolution principlecomputer studiesHilbert-type propositional calculiunification theorem

Mathematics Subject Classification ID

History of mathematics in the 20th century (01A60) Mechanization of proofs and logical operations (03B35) History of mathematical logic and foundations (03-03)

Related Items (6)

Searching for circles of pure proofs ⋮ A finitely axiomatized formalization of predicate calculus with equality ⋮ A (machine-oriented) logic based on pattern matching ⋮ Shortest axiomatizations of implicational S4 and S5 ⋮ Implementing the `Fool's model' of combinatory logic ⋮ Learning from Łukasiewicz and Meredith: investigations into proof structures

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The two-property and condensed detachment
• Questions concerning possible shortest single axioms for the equivalential calculus: An application of automated theorem proving to infinite domains
• In memoriam Carew Arthur Meredith (1904-1976)
• An automatic theorem prover for substitution and detachment systems
• A shortest single axiom for the classical equivalential calculus
• An improved proof procedure1
• Methods for Automated Theorem Proving in Nonclassical Logics
• A Machine-Oriented Logic Based on the Resolution Principle
• The logic theorist in LISP†
• A Computing Procedure for Quantification Theory

This page was built for publication: Condensed detachment as a rule of inference