Paper Info
Title
Fast algorithms for testing unsatisfiability of ground horn clauses with equations
Abstract
This paper presents two fast algorithms for testing the unsatisfiability of a set of ground Horn clauses with or without equational atomic formulae. If the length of the set H of Horn clauses (viewed as the string obtained by concatenating the clauses in H) is n, it is possible to design an algorithm running in time O(n log(n)). These algorithms are obtained by generalising the concept of congruence closure to ground Horn clauses. The basic idea behind these algorithms is that the congruence closure induced by a set of ground Horn clauses can be obtained by interleaving steps in which an equational congruence closure is computed, and steps in which an implicational type of closure is computed.
Year
DOI
Venue
1987
10.1016/S0747-7171(87)80067-6
J. Symb. Comput.
Keywords
DocType
Volume
equational atomic formula,Horn clause,basic idea,set H,n log,equational congruence closure,ground Horn clause,ground horn clause,congruence closure,fast algorithm,implicational type
Journal
4
Issue
ISSN
Citations 
2
Journal of Symbolic Computation
2
PageRank 
References 
Authors
0.41
7
1
Name
Order
Citations
PageRank
Jean H. Gallier1749111.86