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 39 articles , 1 standard article )

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

1 2 next

  1. Al-Saedi, Balasim; Fourdrinoy, Olivier; Grégoire, Éric; Mazure, Bertrand; Saïs, Lakhdar: About some UP-based polynomial fragments of SAT (2017)
  2. Gottlob, Georg; Koch, Christoph; Pieris, Andreas: Logic, languages, and rules for web data extraction and reasoning over data (2017)
  3. Kučera, Petr: Hydras: complexity on general graphs and a subclass of trees (2017)
  4. Arif, M.Fareed; Mencía, Carlos; Ignatiev, Alexey; Manthey, Norbert; Peñaloza, Rafael; Marques-Silva, Joao: BEACON: an efficient SAT-based tool for debugging $\mathcal EL^+$ ontologies (2016)
  5. Marques-Silva, Joao; Ignatiev, Alexey; Mencía, Carlos; Peñaloza, Rafael: Efficient reasoning for inconsistent Horn formulae (2016)
  6. Arif, M.Fareed; Mencía, Carlos; Marques-Silva, Joao: Efficient MUS enumeration of Horn formulae with applications to axiom pinpointing (2015)
  7. Mencía, Carlos; Previti, Alessandro; Marques-Silva, Joao: SAT-based Horn least upper bounds (2015)
  8. Boros, Endre; Gruber, Aritanan: Hardness results for approximate pure Horn CNF formulae minimization (2014)
  9. Blass, Andreas; Gurevich, Yuri: Abstract Hilbertian deductive systems, infon logic, and Datalog (2013)
  10. Boros, Endre; Čepek, Ondřej; Kučera, Petr: A decomposition method for CNF minimality proofs (2013)
  11. Čepek, Ondřej; Kučera, Petr; Vlček, Václav: Properties of SLUR formulae (2012)
  12. Gottlob, Georg; Pichler, Reinhard; Wei, Fang: Tractable database design and datalog abduction through bounded treewidth (2010) ioport
  13. Gottlob, Georg; Pichler, Reinhard; Wei, Fang: Bounded treewidth as a key to tractability of knowledge representation and reasoning (2010)
  14. Boros, Endre; Čepek, Ondřej; Kogan, Alexander; Kučera, Petr: A subclass of Horn CNFs optimally compressible in polynomial time (2009)
  15. Champavère, Jér^ome; Gilleron, Rémi; Lemay, Aurélien; Niehren, Joachim: Efficient inclusion checking for deterministic tree automata and XML schemas (2009)
  16. Faber, Wolfgang; Pfeifer, Gerald; Leone, Nicola; Dell’Armi, Tina; Ielpa, Giuseppe: Design and implementation of aggregate functions in the DLV system (2008)
  17. Frühwirth, Thom: Quasi-linear-time algorithms by generalisation of union-find in CHR (2008)
  18. Porschen, Stefan; Speckenmeyer, Ewald: A CNF class generalizing exact linear formulas (2008)
  19. Porschen, Stefan; Speckenmeyer, Ewald: Satisfiability of mixed Horn formulas (2007)
  20. Porschen, Stefan; Speckenmeyer, Ewald: Algorithms for variable-weighted 2-SAT and dual problems (2007)

1 2 next