A finitely axiomatized formalization of predicate calculus with equality

DOI10.1305/ndjfl/1040149359zbMath0838.03008OpenAlexW2020144980MaRDI QIDQ1906674

Norman D. Megill

Publication date: 4 February 1996

Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1305/ndjfl/1040149359

zbMATH Keywords

completenessfinite axiomatizationcondensed detachmentZermelo-Fraenkel set theoryformalization of first-order predicate calculus with equalityresolution-based theorem provers

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35)

Cites Work

• Condensed detachment as a rule of inference
• Set theory in first-order logic: Clauses for Gödel's axioms
• Condensed detachment is complete for relevance logic: A computer-aided proof
• Algebraization of quantifier logics, an introductory overview
• In memoriam Carew Arthur Meredith (1904-1976)
• An automatic theorem prover for substitution and detachment systems
• Principal type-schemes and condensed detachment
• A Machine-Oriented Logic Based on the Resolution Principle
• Substitutionless predicate logic with identity
• A simplified formalization of predicate logic with identity
• On Tarski's formalization of predicate logic with identity
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item