Analytic tableaux for higher-order logic with choice
From MaRDI portal
Publication:5747752
DOI10.1007/978-3-642-14203-1_7zbMATH Open1291.03015OpenAlexW126011539MaRDI QIDQ5747752FDOQ5747752
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
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
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- Title not available (Why is that?)
- TPS: A hybrid automatic-interactive system for developing proofs
- Title not available (Why is that?)
- Cut-elimination for simple type theory with an axiom of choice
- Higher-order semantics and extensionality
- Completeness in the theory of types
- Resolution in type theory
- Extended First-Order Logic
- Analytic Tableaux for Simple Type Theory and its First-Order Fragment
- Terminating tableaux for the basic fragment of simple type theory
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- General models and extensionality
- Analytic tableaux for higher-order logic with choice
- Title not available (Why is that?)
Cited In (11)
- Extending Sledgehammer with SMT solvers
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- Analytic tableaux for positive logic free from ``paradoxes of material implication
- The expected complexity of analytic tableaux analyses in propositional calculus. II
- Analytic tableaux for higher-order logic with choice
- Reducing higher-order theorem proving to a sequence of SAT problems
- Combining and automating classical and non-classical logics in classical higher-order logics
- Reducing higher-order theorem proving to a sequence of SAT problems
- A bibliography on analytic tableaux theorem proving
- Analytic tableaux for higher-order logic with choice
- Title not available (Why is that?)
Uses Software
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)
