Analytic tableaux for higher-order logic with choice
DOI10.1007/S10817-011-9233-2zbMATH Open1258.03019OpenAlexW2081512679MaRDI QIDQ438561FDOQ438561
Authors: Julian Backes, Chad E. Brown 
Publication date: 31 July 2012
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-011-9233-2
Recommendations
axiom of choiceautomated theorem provinghigher-order logicHenkin modelshigher-order automated theorem-prover \texttt{Satallax}simple type theory with choicetableau calculus
Mechanization of proofs and logical operations (03B35) Axiom of choice and related propositions (03E25)
Cites Work
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- Theory and Applications of Satisfiability Testing
- A Brief Overview of HOL4
- Title not available (Why is that?)
- TPS: A hybrid automatic-interactive system for developing proofs
- Isabelle/HOL. A proof assistant for higher-order logic
- Functional and Logic Programming
- Title not available (Why is that?)
- A formulation of the simple theory of types
- Cut-Simulation and Impredicativity
- Cut-elimination for simple type theory with an axiom of choice
- Higher-order semantics and extensionality
- Completeness in the theory of types
- A compact representation of proofs
- Automated reasoning in higher-order logic. Set comprehension and extensionality in Church's type theory
- Resolution in type theory
- Labelling techniques and typed fixed-point operators
- 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
- Title not available (Why is that?)
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- Hauptsatz for higher order logic
- Simple type theory of Gentzen style with the inference of extensionality
- Title not available (Why is that?)
- General models and extensionality
- A UNIFYING PRINCIPAL IN QUANTIFICATION THEORY
- Analytic tableaux for higher-order logic with choice
Cited In (15)
- Superposition with lambdas
- Lash 1.0 (system description)
- Analytic tableaux for positive logic free from ``paradoxes of material implication
- The expected complexity of analytic tableaux analyses in propositional calculus. II
- Cut-elimination for quantified conditional logic
- The higher-order prover \textsc{Leo}-II
- Analytic tableaux for higher-order logic with choice
- Making higher-order superposition work
- Superposition with lambdas
- A bibliography on analytic tableaux theorem proving
- Satallax
- Making higher-order superposition work
- The CADE-26 automated theorem proving system competition – CASC-26
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
- 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 Q438561)
