Unification as a complexity measure for logic programming
DOI10.1016/0743-1066(87)90014-8zbMATH Open0641.68143OpenAlexW2021929022MaRDI QIDQ3782840FDOQ3782840
Authors: Alon Itai, Johann A. Makowsky 
Publication date: 1987
Published in: The Journal of Logic Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0743-1066(87)90014-8
Recommendations
hierarchycomputational completenessTuring computabilityunificationlogic programmingTuring machinesHorn clausecomplexity measure
Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (34)
- A decomposition method for CNF minimality proofs
- Abstract Hilbertian deductive systems, infon logic, and Datalog
- The possibilistic Horn non-clausal knowledge bases
- A subclass of Horn CNFs optimally compressible in polynomial time
- Selective Unification in (Constraint) Logic Programming*
- An \(O(n^ 2)\) algorithm for the satisfiability problem of a subset of propositional sentences in CNF that includes all Horn sentences
- Bidual Horn functions and extensions
- An incremental algorithm for generating all minimal models
- Unique satisfiability of Horn sets can be solved in nearly linear time
- Straight-line program length as a parameter for complexity measures
- BEACON: an efficient SAT-based tool for debugging \(\mathcal {EL}^+\) ontologies
- 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
- Directed hypergraphs and applications
- Reasoning with minimal models: efficient algorithms and applications
- Maximum renamable Horn sub-CNFs
- Properties of SLUR Formulae
- Hardness results for approximate pure Horn CNF formulae minimization
- An efficient labelled nested multiset unification algorithm
- Capturing complexity classes by fragments of second-order logic
- The Qu-Prolog unification algorithm: formalisation and correctness
- Model Checking Games
- On computing minimal models
- Counting truth assignments of formulas of bounded tree-width or clique-width
- Sorting, linear time and the satisfiability problem
- Efficient reasoning for inconsistent Horn formulae
- Hypergraph Horn functions
- Title not available (Why is that?)
- A new combination of input and unit deductions for Horn sentences
- Title not available (Why is that?)
- SAT-Based Horn Least Upper Bounds
- Hydras: complexity on general graphs and a subclass of trees
- Title not available (Why is that?)
- Efficient MUS enumeration of Horn formulae with applications to axiom pinpointing
This page was built for publication: Unification as a complexity measure for logic programming
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3782840)
