Proof-Theoretic Soundness and Completeness
Robert Rothenberg
TL;DR
This paper introduces a calculus for first-order classical logic that aligns with intuitionistic Kripke semantics and provides a proof-theoretic framework for soundness and completeness, facilitating automation.
Contribution
It presents a new calculus for first-order classical logic with proof-theoretic soundness and completeness tailored for intuitionistic Kripke frames, aiding automated reasoning.
Findings
Calibrated a calculus for first-order classical logic.
Established proof-theoretic soundness and completeness.
Facilitated potential automation of reasoning processes.
Abstract
We give a calculus for reasoning about the first-order fragment of classical logic that is adequate for giving the truth conditions of intuitionistic Kripke frames, and outline a proof-theoretic soundness and completeness proof, which we believe is conducive to automation.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Logic, programming, and type systems · Semantic Web and Ontologies