Analytic tableaux for higher-order logic with choice

DOI10.1007/S10817-011-9233-2MaRDI QIDQ438561zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

axiom of choiceautomated theorem provinghigher-order logicHenkin modelshigher-order automated theorem-prover \texttt{Satallax}simple type theory with choicetableau calculus

Mathematics Subject Classification ID

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

Recommendations

• Analytic tableaux for higher-order logic with choice
• scientific article; zbMATH DE number 1552534
• Analytic Tableaux for Simple Type Theory and its First-Order Fragment
• scientific article; zbMATH DE number 1301855
• A Focused Sequent Calculus for Higher-Order Logic

Cites work

• scientific article; zbMATH DE number 1303341 (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?)
• scientific article; zbMATH DE number 3395450 (Why is no real title available?)
• A Brief Overview of HOL4
• A UNIFYING PRINCIPAL IN QUANTIFICATION THEORY
• A compact representation of proofs
• A formulation of the simple theory of types
• Analytic Tableaux for Simple Type Theory and its First-Order Fragment
• Analytic tableaux for higher-order logic with choice
• Automated reasoning in higher-order logic. Set comprehension and extensionality in Church's type theory
• Completeness in the theory of types
• Cut-Simulation and Impredicativity
• Cut-elimination for simple type theory with an axiom of choice
• Extended First-Order Logic
• Functional and Logic Programming
• General models and extensionality
• Hauptsatz for higher order logic
• Higher-order semantics and extensionality
• Isabelle/HOL. A proof assistant for higher-order logic
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• Labelling techniques and typed fixed-point operators
• Progress in the Development of Automated Theorem Proving for Higher-Order Logic
• Resolution in type theory
• Simple type theory of Gentzen style with the inference of extensionality
• TPS: A hybrid automatic-interactive system for developing proofs
• Terminating tableaux for the basic fragment of simple type theory
• Theory and Applications of Satisfiability Testing

Cited in

(15)

• Cut-elimination for quantified conditional logic
• A bibliography on analytic tableaux theorem proving
• The higher-order prover \textsc{Leo}-II
• Analytic tableaux for higher-order logic with choice
• The CADE-26 automated theorem proving system competition -- CASC-26
• Satallax
• scientific article; zbMATH DE number 1552534 (Why is no real title available?)
• Making higher-order superposition work
• Superposition with lambdas
• Superposition with lambdas
• Analytic tableaux for positive logic free from ``paradoxes of material implication
• Lash 1.0 (system description)
• Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
• Making higher-order superposition work
• The expected complexity of analytic tableaux analyses in propositional calculus. II

Describes a project that uses

Uses Software

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

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)