Hornlog: A graph-based interpreter for general Horn clauses. In this very interesting paper a new method is presented for logic- programming interpreters based on graph rewriting and on a linear-time algorithm for showing the unsatisfiability of ground Horn clauses. The method (called Hornlog) applies to a class of logic programs that is a proper extension of the class that consists of what are normally called Horn clauses, but is still strictly included in the class of first-order formulas. In particular, negative Horn clauses can be used as assertions and also queries consisting of disjunctions of negations of Horn clauses are allowed. It is possible in this class to state some forms of negation without resort to negation-as-failure semantics. Moreover, it is possible to yield indefinite answers, i.e. disjunctions of substitutions. The method seems particularly useful for implementation in a parallel environment.
Keywords for this software
References in zbMATH (referenced in 6 articles , 1 standard article )
Showing results 1 to 6 of 6.
- Stabler, Edward P. jun.: Parsing as non-Horn deduction (1993)
- Miller, Dale; Nadathur, Gopalan; Pfenning, Frank; Scedrov, Andre: Uniform proofs as a foundation for logic programming (1991)
- Chandru, Vijaya; Coullard, Collette R.; Hammer, Peter L.; Montañez, Miguel; Sun, Xiaorong: On renamable Horn and generalized Horn functions (1990)
- Minoux, M.; Barkaoui, K.: Deadlocks and traps in Petri nets as Horn-satisfiability solutions and some related polynomially solvable problems (1990)
- Minoux, Michel: LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation (1988)
- Gallier, Jean H.; Raatz, Stan: Hornlog: A graph-based interpreter for general Horn clauses (1987)