Analytic tableaux for higher-order logic with choice

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

zbMATH Keywords

higher-order logicaxiom of choiceautomated theorem provingtableau calculusHenkin modelshigher-order automated theorem-prover \texttt{Satallax}simple type theory with choice

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Axiom of choice and related propositions (03E25)

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

• MiniSat
• TPS
• ML
• Isabelle/HOL
• HOL
• HOL Light

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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