Unification as a complexity measure for logic programming

DOI10.1016/0743-1066(87)90014-8zbMath0641.68143OpenAlexW2021929022MaRDI QIDQ3782840

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

zbMATH Keywords

Turing machinesunificationlogic programminghierarchyTuring computabilitycomputational completenessHorn clausecomplexity measure

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (31)

Properties of SLUR Formulae ⋮ Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing ⋮ SAT-Based Horn Least Upper Bounds ⋮ Unique satisfiability of Horn sets can be solved in nearly linear time ⋮ An \(O(n^ 2)\) algorithm for the satisfiability problem of a subset of propositional sentences in CNF that includes all Horn sentences ⋮ The Qu-Prolog unification algorithm: formalisation and correctness ⋮ Polynomial-time inference of all valid implications for Horn and related formulae ⋮ An efficient labelled nested multiset unification algorithm ⋮ Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing ⋮ On computing minimal models ⋮ Reasoning with minimal models: efficient algorithms and applications ⋮ A decomposition method for CNF minimality proofs ⋮ Abstract Hilbertian deductive systems, infon logic, and Datalog ⋮ Maximum renamable Horn sub-CNFs ⋮ Bidual Horn functions and extensions ⋮ An incremental algorithm for generating all minimal models ⋮ Hydras: complexity on general graphs and a subclass of trees ⋮ Capturing complexity classes by fragments of second-order logic ⋮ Counting truth assignments of formulas of bounded tree-width or clique-width ⋮ Model Checking Games ⋮ Hardness results for approximate pure Horn CNF formulae minimization ⋮ A subclass of Horn CNFs optimally compressible in polynomial time ⋮ Hypergraph Horn functions ⋮ Unnamed Item ⋮ Directed hypergraphs and applications ⋮ BEACON: An Efficient SAT-Based Tool for Debugging $${\mathcal {EL}}{^+}$$ Ontologies ⋮ Unnamed Item ⋮ Sorting, linear time and the satisfiability problem ⋮ Efficient Reasoning for Inconsistent Horn Formulae ⋮ A new combination of input and unit deductions for Horn sentences ⋮ The possibilistic Horn non-clausal knowledge bases

This page was built for publication: Unification as a complexity measure for logic programming