Unification as a complexity measure for logic programming

DOI10.1016/0743-1066(87)90014-8MaRDI QIDQ3782840zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

hierarchycomputational completenessTuring computabilityunificationlogic programmingTuring machinesHorn clausecomplexity measure

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 3995082
• On computability by logic programs
• scientific article; zbMATH DE number 4103047
• scientific article; zbMATH DE number 6917940
• Alternation and the computational complexity of logic programs

Cited in

(34)

• A decomposition method for CNF minimality proofs
• Abstract Hilbertian deductive systems, infon logic, and Datalog
• Efficient MUS enumeration of Horn formulae with applications to axiom pinpointing
• 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
• BEACON: an efficient SAT-based tool for debugging \(\mathcal {EL}^+\) ontologies
• Polynomial-time inference of all valid implications for Horn and related formulae
• Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing
• Straight-line program length as a parameter for complexity measures
• 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
• Capturing complexity classes by fragments of second-order logic
• An efficient labelled nested multiset unification algorithm
• The Qu-Prolog unification algorithm: formalisation and correctness
• On computing minimal models
• Model Checking Games
• 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
• A new combination of input and unit deductions for Horn sentences
• Hypergraph Horn functions
• scientific article; zbMATH DE number 6820296 (Why is no real title available?)
• scientific article; zbMATH DE number 3921947 (Why is no real title available?)
• Hydras: complexity on general graphs and a subclass of trees
• SAT-Based Horn Least Upper Bounds
• scientific article; zbMATH DE number 6917940 (Why is no real title available?)

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)