Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory

DOI10.1007/978-3-031-38499-8_28MaRDI QIDQ6492764

Lukas Stevens

Publication date: 26 April 2024

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• The automation of syllogistic. II: Optimization and complexity issues
• Formalizing a Seligman-style tableau system for hybrid logic (short paper)
• A verified decision procedure for orders in Isabelle/HOL
• Soundness and completeness proofs by coinductive methods
• A henkin-style completeness proof for the modal logic S5
• Completeness and Decidability Results for CTL in Coq
• Linear Quantifier Elimination
• Verifying Mixed Real-Integer Quantifier Elimination
• Decision procedures for elementary sublanguages of set theory. I. Multi-level syllogistic and some extensions
• A fast saturation strategy for set-theoretic tableaux
• A Decision Procedure for a Sublanguage of Set Theory Involving Monotone, Additive, and Multiplicative Functions1 1This research has been partially supported by MURST Grant prot. 2001017741 under project “Ragionamento su aggregati e numeri a supporto della programmazione e relative verifiche”.
• Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
• A sequent calculus for first-order logic formalized in Isabelle/HOL

This page was built for publication: Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory