An Efficient Unification Algorithm
From MaRDI portal
Publication:3936229
DOI10.1145/357162.357169zbMath0478.68093WikidataQ56092428 ScholiaQ56092428MaRDI QIDQ3936229
Ugo Montanari, Alberto Martelli
Publication date: 1982
Published in: ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/357162.357169
resolution; unification problem; mechanical theorem proving; nondeterministic algorithm; complexity of proof procedures
03B10: Classical first-order logic
03B35: Mechanization of proofs and logical operations
03F20: Complexity of proofs
Related Items
Speeding up algorithms on atomic representations of Herbrand models via new redundancy criteria, Automata-driven efficient subterm unification, Constructive negation and constraint logic programming with sets, A non-ground realization of the stable and well-founded semantics, Lazy narrowing: strong completeness and eager variable elimination, Computing minimal models by partial instantiation, A combinatory logic approach to higher-order E-unification, Average-case analysis of unification algorithms, An intensional epistemic logic, A note on the parallel complexity of anti-unification, Unfold/fold transformation of stratified programs, Horn clause programs with polymorphic types: Semantics and resolution, Completion for unification, The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning, Contraction algebras and unification of (infinite) terms, Combining matching algorithms: The regular case, An order-sorted logic for knowledge representation systems, Generalizing completeness results for loop checks in logic programming, An improved general \(E\)-unification method, Probabilistic logic programming, C-expressions: A variable-free calculus for equational logic programming, How to win a game with features, Unification problem in equational theories, A proof procedure for the logic of hereditary Harrop formulas, A semantical framework for supporting subjective and conditional probabilities in deductive databases, Weighted systems of equations, On the duality of abduction and model generation in a framework for model generation with equality, Competing for the \(AC\)-unification race, Computing definite logic programs by partial instantiation, Completeness results for basic narrowing, Accelerating tableaux proofs using compact representations, Definite clause programs are canonical (over a suitable domain), Unification in sort theories and its applications, Deciding the word problem in the union of equational theories., On the complexity of equational problems in CNF, Binary decision diagrams for first-order predicate logic., Relaxed unification -- proposal, On deciding subsumption problems, Explicit versus implicit representations of subsets of the Herbrand universe., Higher order unification via explicit substitutions, Complexity of nilpotent unification and matching problems., Pair-independence and freeness analysis through linear refinement., Nominal unification, Generalizing theorems in real closed fields, Kinded type inference for parametric overloading, Data storage interpretation of labeled modal logic, Higher-order unification via combinators, Source-tracking unification, Unnamed Item
