
GHC
 Referenced in 43 articles
[sw23765]
 Guarded Horn Clauses was born from the examination of existing logic programming languages and logic ... resolutionbased theorem prover for Hornclause 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...

Teyjus
 Referenced in 17 articles
[sw21364]
 Harrop formulas, a logic that significantly extends the theory of Horn clauses. A systematic exploitation...

Hornlog
 Referenced in 6 articles
[sw21362]
 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...

VeriMAP
 Referenced in 11 articles
[sw22866]
 VeriMAP: Transformationaided Horn Clause Verification. VeriMAP is a tool for supporting CHC software verifiers ... been developed in the fields of constraint logic programming and SMT solving...

NuprlLight
 Referenced in 1 article
[sw31982]
 critical part of theorem proving in these logics, the implementation framework is tied closely ... prover, NuprlLight uses generalized Horn clauses for logical specification. Indeed, specifications in NuprlLight...

TreeAutomizer
 Referenced in 3 articles
[sw40819]
 clauses. Constrained Horn clauses (CHC) are a fragment of first order logic with attractive properties...

MGTP
 Referenced in 7 articles
[sw09701]
 based theorem prover MGTP for firstorder logic. This paper describes the major results ... parallelism for nonHorn 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...

Propositional Resolution
 Referenced in 1 article
[sw28841]
 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...

Coq
 Referenced in 1898 articles
[sw00161]
 Coq is a formal proof management system. It...

Isabelle
 Referenced in 714 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows...

MiniSat
 Referenced in 566 articles
[sw00577]
 An extensible SATsolver. MiniSat is a minimalistic...

SETHEO
 Referenced in 122 articles
[sw00707]
 SETHEO: A highperformance theorem prover. The paper...

ML
 Referenced in 522 articles
[sw01218]
 ML (’Meta Language’) is a generalpurpose functional...

ALGOL 68
 Referenced in 291 articles
[sw01226]
 ALGOL 68 (short for ALGOrithmic Language 1968) is...

Beluga
 Referenced in 26 articles
[sw01321]
 Our main interest in this project is to...

CPnets
 Referenced in 138 articles
[sw01374]
 CPnets (Condition Preference Nets) is a tool...

SATLIB
 Referenced in 59 articles
[sw02107]
 SATLIB is a collection of benchmark problems, solvers...

LARCH
 Referenced in 104 articles
[sw02126]
 The Larch family of languages supports a two...

CASL
 Referenced in 174 articles
[sw02235]
 The specification language developed by CoFI is called...

TAPS
 Referenced in 19 articles
[sw02244]
 TAPS: A firstorder verifier for cryptographic protocols...