Ltur

swMATH11689MaRDI QIDQ23629FDOQ23629

Author name not available (Why is that?)

Described by source

• LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation

Cited In (38)

• A decomposition method for CNF minimality proofs
• Abstract Hilbertian deductive systems, infon logic, and Datalog
• A CNF Class Generalizing Exact Linear Formulas
• Bounded treewidth as a key to tractability of knowledge representation and reasoning
• Title not available (Why is that?)
• Satisfiability of mixed Horn formulas
• A subclass of Horn CNFs optimally compressible in polynomial time
• The unique Horn-satisfiability problem and quadratic Boolean equations.
• On the complexity of propositional knowledge base revision, updates, and counterfactuals
• Inferring minimal functional dependencies in Horn and q-Horn theories
• Algorithms for Variable-Weighted 2-SAT and Dual Problems
• Efficient inclusion checking for deterministic tree automata and XML schemas
• Quasi-Linear-Time Algorithms by Generalisation of Union-Find in CHR
• Theory and Applications of Satisfiability Testing
• Horn functions and their DNFs
• Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing
• Polynomial-time inference of all valid implications for Horn and related formulae
• On functional dependencies in \(q\)-Horn theories
• Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing
• On Tackling Explanation Redundancy in Decision Trees
• Properties of SLUR Formulae
• Hardness results for approximate pure Horn CNF formulae minimization
• BEACON: An Efficient SAT-Based Tool for Debugging $${\mathcal {EL}}{^+}$$ Ontologies
• Generalized domination in closure systems
• Branch-and-cut solution of inference problems in propositional logic
• A variant of Reiter's hitting-set algorithm
• Complexity classifications of Boolean constraint satisfaction problems
• Extended Horn sets in propositional logic
• Sorting, linear time and the satisfiability problem
• Logic, Languages, and Rules for Web Data Extraction and Reasoning over Data
• Deadlocks and traps in Petri nets as Horn-satisfiability solutions and some related polynomially solvable problems
• Linear time Datalog and branching time logic
• Design and implementation of aggregate functions in the DLV system
• SAT-Based Horn Least Upper Bounds
• Hydras: complexity on general graphs and a subclass of trees
• About some UP-based polynomial fragments of SAT
• From simplification to a partial theory solver for non-linear real polynomial constraints
• Efficient Reasoning for Inconsistent Horn Formulae

This page was built for software: Ltur