Analytic tableaux for higher-order logic with choice

DOI10.1007/978-3-642-14203-1_7MaRDI QIDQ5747752zbMATHOpenAlexFDO

Authors Julian Backes, Chad E. Brown

Publication date 14 September 2010

Published in Automated Reasoning (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Analytic tableaux for higher-order logic with choice
• Analytic Tableaux for Simple Type Theory and its First-Order Fragment
• scientific article; zbMATH DE number 1552534
• Decision procedures for elementary sublanguages of set theory: XII. Multilevel syllogistic extended with singleton and choice operators
• scientific article; zbMATH DE number 1301855

Cites work

• scientific article; zbMATH DE number 2110621 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• Analytic Tableaux for Simple Type Theory and its First-Order Fragment
• Analytic tableaux for higher-order logic with choice
• Completeness in the theory of types
• Cut-elimination for simple type theory with an axiom of choice
• Extended First-Order Logic
• General models and extensionality
• Higher-order semantics and extensionality
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• Progress in the Development of Automated Theorem Proving for Higher-Order Logic
• Resolution in type theory
• TPS: A hybrid automatic-interactive system for developing proofs
• Terminating tableaux for the basic fragment of simple type theory

Cited in

(11)

• A bibliography on analytic tableaux theorem proving
• Extending Sledgehammer with SMT solvers
• Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
• Reducing higher-order theorem proving to a sequence of SAT problems
• Analytic tableaux for higher-order logic with choice
• Analytic tableaux for higher-order logic with choice
• scientific article; zbMATH DE number 1552534 (Why is no real title available?)
• Analytic tableaux for positive logic free from ``paradoxes of material implication
• Combining and automating classical and non-classical logics in classical higher-order logics
• Reducing higher-order theorem proving to a sequence of SAT problems
• The expected complexity of analytic tableaux analyses in propositional calculus. II

Describes a project that uses

Uses Software

• LEO-II
• TPS
• Satallax

This page was built for publication: Analytic tableaux for higher-order logic with choice

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