Analytic Tableaux for Higher-Order Logic with Choice

DOI10.1007/978-3-642-14203-1_7zbMath1291.03015OpenAlexW126011539MaRDI QIDQ5747752

Julian Backes, Chad Edward 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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (7)

Analytic tableaux for higher-order logic with choice ⋮ Combining and automating classical and non-classical logics in classical higher-order logics ⋮ Analytic Tableaux for Higher-Order Logic with Choice ⋮ Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners) ⋮ Extending Sledgehammer with SMT Solvers ⋮ Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems ⋮ Reducing higher-order theorem proving to a sequence of SAT problems

Uses Software

• LEO-II
• TPS
• Satallax

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• TPS: A hybrid automatic-interactive system for developing proofs
• Extended First-Order Logic
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• Analytic Tableaux for Simple Type Theory and its First-Order Fragment
• 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
• Higher-order semantics and extensionality
• Resolution in type theory
• General models and extensionality
• Analytic Tableaux for Higher-Order Logic with Choice
• Completeness in the theory of types

This page was built for publication: Analytic Tableaux for Higher-Order Logic with Choice