A Free Variable Version of the First-Order Predicate Calculus

DOI10.1093/LOGCOM/1.4.431MaRDI QIDQ3985544zbMATH OpenOpenAlexFDO

Authors Ronald Fechter, Martin Davis

Publication date 27 June 1992

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/logcom/1.4.431

zbMATH Keywords

epsilon calculusfree variable version of first-order predicate calculusresolutionSkolem functionsunification

Mathematics Subject Classification ID

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

Recommendations

• A Free-Variable Theory of Primitive Recursive Arithmetic
• Equational methods in first order predicate calculus
• A free variable sequent calculus with uniform variable splitting
• Automated Reasoning with Analytic Tableaux and Related Methods
• scientific article; zbMATH DE number 432735

Cited in

(11)

• A variable-free logic for mass terms
• A derived algorithm for evaluating -expressions over abstract sets
• scientific article; zbMATH DE number 432735 (Why is no real title available?)
• Banishing ultrafilters from our consciousness
• Semantic Completeness of Free-Variable Theories
• scientific article; zbMATH DE number 4037808 (Why is no real title available?)
• scientific article; zbMATH DE number 1189105 (Why is no real title available?)
• Martin Davis: an overview of his work in logic, computer science, and philosophy
• A simplified proof of the epsilon theorems
• Subject-predicate calculus free from existential import
• A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux

This page was built for publication: A Free Variable Version of the First-Order Predicate Calculus

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