Analytic tableaux for higher-order logic with choice
From MaRDI portal
Publication:438561
DOI10.1007/s10817-011-9233-2zbMath1258.03019OpenAlexW2081512679MaRDI QIDQ438561
Julian Backes, Chad Edward 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
higher-order logicaxiom of choiceautomated theorem provingtableau calculusHenkin modelshigher-order automated theorem-prover \texttt{Satallax}simple type theory with choice
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (10)
Cut-elimination for quantified conditional logic ⋮ The higher-order prover \textsc{Leo}-II ⋮ The CADE-26 automated theorem proving system competition – CASC-26 ⋮ Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. ⋮ Superposition with lambdas ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ Superposition with lambdas ⋮ Satallax ⋮ Lash 1.0 (system description)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- TPS: A hybrid automatic-interactive system for developing proofs
- A compact representation of proofs
- Isabelle/HOL. A proof assistant for higher-order logic
- Extended First-Order Logic
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- A Brief Overview of HOL4
- Analytic Tableaux for Simple Type Theory and its First-Order Fragment
- Cut-Simulation and Impredicativity
- Terminating Tableaux for the Basic Fragment of Simple Type Theory
- Cut-elimination for simple type theory with an axiom of choice
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- Functional and Logic Programming
- Higher-order semantics and extensionality
- Theory and Applications of Satisfiability Testing
- Hauptsatz for higher order logic
- Simple type theory of Gentzen style with the inference of extensionality
- Resolution in type theory
- General models and extensionality
- A UNIFYING PRINCIPAL IN QUANTIFICATION THEORY
- Analytic Tableaux for Higher-Order Logic with Choice
- A formulation of the simple theory of types
- Completeness in the theory of types
This page was built for publication: Analytic tableaux for higher-order logic with choice
