A framework for using knowledge in tableau proofs

DOI10.1007/BFB0027424MaRDI QIDQ4610337zbMATH OpenOpenAlexFDO

Authors Benjamin Shults

Publication date 15 January 2019

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bfb0027424

zbMATH Keywords

knowledge baseautomated deductionsequent calculusautomated reasoningconjunctive normal form

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief
• scientific article; zbMATH DE number 1612565
• scientific article; zbMATH DE number 1543300
• scientific article; zbMATH DE number 2099386
• Knowledge-based proof planning
• TABLEAUX: A general theorem prover for modal logics
• Formally verified tableau-based reasoners for a description logic
• A propositional tableaux based proof calculus for reasoning with default rules
• scientific article; zbMATH DE number 2090533
• Prefixed tableau systems for logic of proofs and provability

Cites work

• scientific article; zbMATH DE number 3112450 (Why is no real title available?)
• scientific article; zbMATH DE number 1330425 (Why is no real title available?)
• scientific article; zbMATH DE number 1348484 (Why is no real title available?)
• scientific article; zbMATH DE number 517067 (Why is no real title available?)
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• A beginner's further guide to mathematical logic
• A completion-based method for mixed universal and rigid \(E\)-unification
• A-ordered tableaux
• An algorithm for reasoning about equality
• Controlled integration of the cut rule into connection tableau calculi
• Fast Decision Procedures Based on Congruence Closure
• Gazing: An approach to the problem of definition and lemma use
• Hyper tableaux
• Manifolds, tensor analysis, and applications.
• SETHEO: A high-performance theorem prover
• The liberalized -rule in free variable semantic tableaux
• Towards the automation of set theory and its logic

Cited in

(1)

• A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief

Describes a project that uses

Uses Software

• SETHEO

This page was built for publication: A framework for using knowledge in tableau proofs

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