Tableaux for projection computation and knowledge compilation

DOI10.1007/978-3-642-02716-1_24MaRDI QIDQ3648738zbMATH OpenOpenAlexFDO

Authors Christoph Wernhard

Publication date 1 December 2009

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

Full work available at URL https://doi.org/10.1007/978-3-642-02716-1_24

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Quantifier elimination, model completeness, and related topics (03C10)

Recommendations

• Automated deduction for projection elimination.
• A tableaux calculus for reducing proof size
• Literal Projection for First-Order Logic
• Tableaux, path dissolution, and decomposable negation normal form for knowledge compilation
• Normal Forms for Knowledge Compilation

Cited in

(7)

• Precise quantitative information flow analysis -- a symbolic approach
• Incremental Tabling in Support of Knowledge Representation and Reasoning
• Second-order quantifier elimination on relational monadic formulas -- a basic method and some less expected applications
• Literal Projection for First-Order Logic
• Automated deduction for projection elimination.
• Projection and scope-determined circumscription
• Tableaux, path dissolution, and decomposable negation normal form for knowledge compilation

This page was built for publication: Tableaux for projection computation and knowledge compilation

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