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

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

1 2 next

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

1 2 next