Tableaux for First Order Logic of Proofs
Meghdad Ghari
TL;DR
This paper introduces a tableau proof system for first order logic of proofs, demonstrating its soundness and completeness relative to Mkrtychev models, advancing formal proof methods.
Contribution
It presents the first tableau proof system for FOLP and proves its soundness and completeness, enhancing proof theory for this logic.
Findings
Tableau system for FOLP is sound.
Tableau system for FOLP is complete.
System aligns with Mkrtychev models.
Abstract
In this paper we present a tableau proof system for first order logic of proofs FOLP. We show that the tableau system is sound and complete with respect to Mkrtychev models of FOLP.
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 · Advanced Algebra and Logic · Logic, programming, and type systems