Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems

DOI10.1007/978-3-642-22438-6_13zbMath1314.68275OpenAlexW2143415975MaRDI QIDQ5200021

Chad Edward Brown

Publication date: 29 July 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22438-6_13

zbMATH Keywords

higher-order logicSAT solvinghigher-order theorem provingsimple type theoryabstract consistency

Mathematics Subject Classification ID

Related Items (1)

Reducing higher-order theorem proving to a sequence of SAT problems

Uses Software

• LEO-II
• MiniSat
• TPS
• TPTP
• Satallax
• Sledgehammer
• iProver

Cites Work

• TPS: A hybrid automatic-interactive system for developing proofs
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Analytic Tableaux for Simple Type Theory and its First-Order Fragment
• Theory and Applications of Satisfiability Testing
• A UNIFYING PRINCIPAL IN QUANTIFICATION THEORY
• Analytic Tableaux for Higher-Order Logic with Choice
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems