An Efficient Unification Algorithm
From MaRDI portal
Publication:3936229
DOI10.1145/357162.357169zbMath0478.68093OpenAlexW2113722134WikidataQ56092428 ScholiaQ56092428MaRDI QIDQ3936229
Alberto Martelli, Ugo Montanari
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
resolutionunification problemmechanical theorem provingnondeterministic algorithmcomplexity of proof procedures
Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)
Related Items
Computing definite logic programs by partial instantiation, Pair-independence and freeness analysis through linear refinement., Completeness results for basic narrowing, Effective codescent morphisms in the varieties determined by convergent term rewriting systems., A parallel algorithm for the monadic unification problem, Accelerating tableaux proofs using compact representations, Unification for infinite sets of equations between finite terms, Nominal unification, TWAM: a certifying abstract machine for logic programs, Nominal unification with atom-variables, Associative-commutative unification, Unification problems with one-sided distributivity, Unification in combinations of collapse-free regular theories, Termination of floating-point computations, Generalizing theorems in real closed fields, Definite clause programs are canonical (over a suitable domain), A practically efficient and almost linear unification algorithm, A unification algorithm for second-order monadic terms, Representing and building models for decidable subclasses of equational clausal logic, Some techniques for proving termination of the hyperresolution calculus, Kinded type inference for parametric overloading, Finite generation of ambiguity in context-free languages, Data storage interpretation of labeled modal logic, Unification in sort theories and its applications, Inheritance hierarchies: Semantics and unifications, On the relationship of congruence closure and unification, Equational problems and disunification, Enumerating outer narrowing derivations for constructor-based term rewriting systems, Deciding the word problem in the union of equational theories., Logic programming as classical inference, Herbrand's fundamental theorem in the eyes of Jean van Heijenoort, On the complexity of equational problems in CNF, Term rewriting and beyond -- theorem proving in Isabelle, Type inference with subtypes, Conditional equational theories and complete sets of transformations, Rigid E-unification: NP-completeness and applications to equational matings, Binary decision diagrams for first-order predicate logic., A metamodel of access control for distributed environments: applications and properties, Linearity and iterator types for Gödel's system \(\mathcal T\), Relaxed unification -- proposal, Bounding messages for free in security protocols -- extension to various security properties, 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, 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, An order-sorted logic for knowledge representation systems, Abstract conjunctive partial deduction for the analysis and compilation of coroutines, Average-case analysis of unification algorithms, Generalizing completeness results for loop checks in logic programming, An intensional epistemic logic, A note on the parallel complexity of anti-unification, An improved general \(E\)-unification method, Proximity-based unification theory, A linear algorithm for MLL proof net correctness and sequentialization, Probabilistic logic programming, C-expressions: A variable-free calculus for equational logic programming, Termination of narrowing via termination of rewriting, The correctness of Newman's typability algorithm and some of its extensions, On deciding subsumption problems, Unification in Boolean rings and Abelian groups, An almost linear Robinson unification algorithm, Order-sorted unification, Unification in a combination of arbitrary disjoint equational theories, A sound and complete semantics for a similarity-based logic programming language, Regular expression order-sorted unification and matching, Complete sets of transformations for general E-unification, Adventures in associative-commutative unification, A practical unification algorithm, How to win a game with features, Complete sets of unifiers and matchers in equational theories, Safely composing security protocols, Average-case analysis of Robinson's unification algorithm with two different variables, On the logic of unification, Higher-order unification revisited: Complete sets of transformations, Horn equational theories and paramodulation, An ordering linear unification algorithm, Unification problem in equational theories, On equational theories, unification, and (un)decidability, A hybrid programming scheme combining fuzzy-logic and functional-logic resources, Context unification with one context variable, Explicit versus implicit representations of subsets of the Herbrand universe., Higher order unification via explicit substitutions, Complexity of nilpotent unification and matching problems., Faster linear unification algorithm, 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, Simple second-order languages for which unification is undecidable, Accumulators: New logic variable abstractions for functional languages, Competing for the \(AC\)-unification race, Order-sorted logic programming with predicate hierarchy, Properties of substitutions and unifications, Nominal unification with letrec and environment-variables, Completeness and confluence of order-sorted term rewriting, A new approach to general E-unification based on conditional rewriting systems, An universal termination condition for solving goals in equational languages, Higher-order unification via combinators, Linear unification of higher-order patterns, Alternating two-way AC-tree automata, Goal directed strategies for paramodulation, The negation elimination from syntactic equational formula is decidable, Implementation of a UU-algorithm for primitive recursive tree functions, Efficient Equivalence Checking Technique for Some Classes of Finite-State Machines, Certification of Termination Proofs Using CeTA, Terminological reasoning is inherently intractable, On complexity of the anti-unification problem, A Rewriting Logic Approach to Type Inference, Unification modulo an equality theory for equational logic programming, An efficient labelled nested multiset unification algorithm, General \(E\)-unification with eager variable elimination and a nice cycle rule, Decomposable theories, Nominal Unification and Matching of Higher Order Expressions with Recursive Let, Thresholded semantic framework for a fully integrated fuzzy logic language, Some complexity theoretic aspects of AC rewriting, A matching process modulo a theory of categorical products, Verification of logic programs with delay declarations, Lazy narrowing: Strong completeness and eager variable elimination (extended abstract), Incremental methods for optimizing partial instantiation, Unnamed Item, Seeking a safe and efficient similarity-based unfolding rule, Concolic testing in logic programming, Typed SLD-resolution: dynamic typing for logic programming, Constraint and Logic Programming: Ugo Montanari’s Main Contributions and Introduction to the Volume Section, Models of Computation: A Tribute to Ugo Montanari’s Vision, Ugo Montanari and Friends, Towards automated deduction in cP systems, The fuzzy logic programming language FASILL: design and implementation, A modular order-sorted equational generalization algorithm, Automatic theorem proving. II, Unnamed Item, Fuzzy lattice operations on first-order terms over signatures with similar constructors: a constraint-based approach, Unnamed Item, Logic and functional programming by retractions : operational semantics, Functional Logic Programming in Maude, T-string unification: Unifying prefixes in non-classical proof methods, Proof-search in intuitionistic logic based on constraint satisfaction, Unification and matching modulo nilpotence, Order-sorted Equational Unification Revisited, Speeding up algorithms on atomic representations of Herbrand models via new redundancy criteria, Symbolic protocol analysis for monoidal equational theories, Analogy in Automated Deduction: A Survey, Automata-driven efficient subterm unification, Constructive negation and constraint logic programming with sets, Non-commutative proof construction: a constraint-based approach, Specifying and Verifying Organizational Security Properties in First-Order Logic, Proving with BDDs and control of information, COCHIS: Stable and coherent implicits, Unification with Singleton Tree Grammars, Automorphisms of types and their applications, Order-Sorted Generalization, Unnamed Item, The CIFF proof procedure for abductive logic programming with constraints: Theory, implementation and experiments, A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method, Connection-based proof construction in linear logic, Vague Domains, S-Unification and Logic Programming, Source-tracking unification, Deduction, Strategies, and Rewriting, An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types, Planning for an Efficient Implementation of Hypothetical Bousi∼Prolog, A freeness and sharing analysis of logic programs based on a pre-interpretation, A formal model for a linear time correctness condition of proof nets of multiplicative linear logic
