LTUR: A simplified linear time unit resolution algorithm for Horn formulae and computer implementation. Testing for the satisfiability of a Horn expression in propositional calculus is a fundamental problem in the area of logic programming for many reasons. Among these is the fact that the basic solution techniques for propositional Horn formulae have been shown to be central to the design of efficient interpreters for some predicate logic-based languages such as Hornlog [J. H. Gallier and S. Raatz, J. Logic Program. 4, 119-155 (1987; Zbl 0641.68145)]. The present paper proposes a simplified way of deriving a linear-time algorithm avoiding many of the intricacies of previously known descriptions. In addition, a full, ready- to-use computer code is provided at the end of the paper together with a detailed analysis of the necessary data structures.

References in zbMATH (referenced in 31 articles , 1 standard article )

Showing results 1 to 20 of 31.
Sorted by year (citations)

1 2 next

  1. Boros, Endre; Gruber, Aritanan: Hardness results for approximate pure Horn CNF formulae minimization (2014)
  2. Blass, Andreas; Gurevich, Yuri: Abstract Hilbertian deductive systems, infon logic, and Datalog (2013)
  3. Boros, Endre; Čepek, Ondřej; Kučera, Petr: A decomposition method for CNF minimality proofs (2013)
  4. Gottlob, Georg; Pichler, Reinhard; Wei, Fang: Bounded treewidth as a key to tractability of knowledge representation and reasoning (2010)
  5. Gottlob, Georg; Pichler, Reinhard; Wei, Fang: Tractable database design and datalog abduction through bounded treewidth (2010)
  6. Boros, Endre; Čepek, Ondřej; Kogan, Alexander; Kučera, Petr: A subclass of Horn CNFs optimally compressible in polynomial time (2009)
  7. Champavère, Jér^ome; Gilleron, Rémi; Lemay, Aurélien; Niehren, Joachim: Efficient inclusion checking for deterministic tree automata and XML schemas (2009)
  8. Faber, Wolfgang; Pfeifer, Gerald; Leone, Nicola; Dell’Armi, Tina; Ielpa, Giuseppe: Design and implementation of aggregate functions in the DLV system (2008)
  9. Frühwirth, Thom: Quasi-linear-time algorithms by generalisation of union-find in CHR (2008)
  10. Porschen, Stefan; Speckenmeyer, Ewald: A CNF class generalizing exact linear formulas (2008)
  11. Porschen, Stefan; Speckenmeyer, Ewald: Algorithms for variable-weighted 2-SAT and dual problems (2007)
  12. Porschen, Stefan; Speckenmeyer, Ewald: Satisfiability of mixed Horn formulas (2007)
  13. Berry, Anne; Sanjuan, Eric; Sigayret, Alain: Generalized domination in closure systems (2006)
  14. Čepek, Ondřej; Kučera, Petr: Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing (2005)
  15. Porschen, Stefan; Speckenmeyer, Ewald: Worst case bounds for some NP-complete modified Horn-SAT problems (2005)
  16. Ibaraki, Toshihide; Kogan, Alexander; Makino, Kazuhisa: Inferring minimal functional dependencies in Horn and q-Horn theories (2003)
  17. Creignou, Nadia; Khanna, Sanjeev; Sudan, Madhu: Complexity classifications of Boolean constraint satisfaction problems (2001)
  18. Ibaraki, Toshihide; Kogan, Alexander; Makino, Kazuhisa: On functional dependencies in $q$-Horn theories (2001)
  19. Wotawa, F.: A variant of Reiter’s hitting-set algorithm (2001)
  20. Gottlob, Georg; Grädel, Erich; Veith, Helmut: Linear time Datalog and branching time logic (2000)

1 2 next