- Referenced in 43 articles
- Guarded Horn Clauses was born from the examination of existing logic programming languages and logic ... resolution-based theorem prover for Horn-clause sentences. The restriction has two aspects ... Although Guarded Horn Clauses can be classified into the family of logic programming languages ... implementation of exhaustive solution search for Horn- clause programs. We showed how to automatically compile...
- Referenced in 17 articles
- Harrop formulas, a logic that significantly extends the theory of Horn clauses. A systematic exploitation...
- Referenced in 6 articles
- Horn clauses. In this very interesting paper a new method is presented for logic- programming ... ground Horn clauses. The method (called Hornlog) applies to a class of logic programs that ... consists of what are normally called Horn clauses, but is still strictly included...
- Referenced in 11 articles
- VeriMAP: Transformation-aided Horn Clause Verification. VeriMAP is a tool for supporting CHC software verifiers ... been developed in the fields of constraint logic programming and SMT solving...
- Referenced in 1 article
- critical part of theorem proving in these logics, the implementation framework is tied closely ... prover, Nuprl-Light uses generalized Horn clauses for logical specification. Indeed, specifications in Nuprl-Light...
- Referenced in 3 articles
- clauses. Constrained Horn clauses (CHC) are a fragment of first order logic with attractive properties...
- Referenced in 7 articles
- based theorem prover MGTP for first-order logic. This paper describes the major results ... parallelism for non-Horn problems and AND parallelism for Horn problems achieving more than ... Horn magic set to suppress the generation of useless model candidates caused by irrelevant clauses ... negation as failure, abductive reasoning and modal logic systems, on MGTP. These techniques share...
- Referenced in 1 article
- completeness of the Resolution rule in propositional logic. The completeness proofs take into account ... refinement is complete only for clause sets that are Horn- renamable). We also define...
- Referenced in 1898 articles
- Coq is a formal proof management system. It...
- Referenced in 714 articles
- Isabelle is a generic proof assistant. It allows...
- Referenced in 566 articles
- An extensible SAT-solver. MiniSat is a minimalistic...
- Referenced in 122 articles
- SETHEO: A high-performance theorem prover. The paper...
- Referenced in 522 articles
- ML (’Meta Language’) is a general-purpose functional...
- Referenced in 291 articles
- ALGOL 68 (short for ALGOrithmic Language 1968) is...
- Referenced in 26 articles
- Our main interest in this project is to...
- Referenced in 138 articles
- CP-nets (Condition Preference Nets) is a tool...
- Referenced in 59 articles
- SATLIB is a collection of benchmark problems, solvers...
- Referenced in 104 articles
- The Larch family of languages supports a two...
- Referenced in 174 articles
- The specification language developed by CoFI is called...
- Referenced in 19 articles
- TAPS: A first-order verifier for cryptographic protocols...