Reducing higher-order theorem proving to a sequence of SAT problems
From MaRDI portal
Publication:2351156
DOI10.1007/s10817-013-9283-8zbMath1314.68276OpenAlexW1997110410MaRDI QIDQ2351156
Publication date: 23 June 2015
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-013-9283-8
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (8)
Eliminating models during model elimination ⋮ The CADE-26 automated theorem proving system competition – CASC-26 ⋮ Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning ⋮ TacticToe: learning to prove with tactics ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ Extracting Higher-Order Goals from the Mizar Mathematical Library ⋮ Theorem proving as constraint solving with coherent logic
Uses Software
Cites Work
- TPS: A hybrid automatic-interactive system for developing proofs
- SET-VAR
- Isabelle/HOL. A proof assistant for higher-order logic
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- 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
- Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems
- A UNIFYING PRINCIPAL IN QUANTIFICATION THEORY
- Analytic Tableaux for Higher-Order Logic with Choice
- iProver-Eq: An Instantiation-Based Theorem Prover with Equality
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Reducing higher-order theorem proving to a sequence of SAT problems
