Properties of substitutions and unifications
From MaRDI portal
Publication:1074342
DOI10.1016/S0747-7171(85)80027-4zbMATH Open0589.68063MaRDI QIDQ1074342FDOQ1074342
Authors: Elmar Eder 
Publication date: 1985
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Recommendations
- scientific article; zbMATH DE number 3858458
- scientific article; zbMATH DE number 3968580
- Higher order unification via explicit substitutions
- Axiomatisation of substitution
- Unification via the \(\lambda s_e\)-style of explicit substitutions
- scientific article; zbMATH DE number 2080005
- Confluence properties of weak and strong calculi of explicit substitutions
- Explicit substitutions and reducibility
- Substitutions into propositional tautologies
Cites Work
- Linear unification
- An Efficient Unification Algorithm
- A Machine-Oriented Logic Based on the Resolution Principle
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- The Concept of Weak Substitution in Theorem-Proving
Cited In (46)
- Reduction of cycle unification of type \(Cpg+r\)
- C-expressions: A variable-free calculus for equational logic programming
- On inductive inference of cyclic structures
- Determinisation of Relational Substitutions in Ordered Categories with Domain
- Improving precision of type analysis using non-discriminative union
- On equational theories, unification, and (un)decidability
- Semantic models for concurrent logic languages
- Title not available (Why is that?)
- Multi-valued logic programming semantics An algebraic approach
- Implication of clauses is undecidable
- On the cardinality computation problem for regular languages over symmetric groups
- Specialisation of Prolog and FCP programs using abstract interpretation
- A non-ground realization of the stable and well-founded semantics
- On the termination of clause graph resolution
- SLDNF resolution with non-safe rule and fixpoint semantics for general logic programs
- Soundness of abductive proof procedure with respect to constraint for non-ground abducibles
- Unification for infinite sets of equations between finite terms
- Title not available (Why is that?)
- Detecting non-provable goals
- Unification in a combination of arbitrary disjoint equational theories
- Epsilon-invariant substitutions and indefinite descriptions
- A compositional semantics for logic programs
- Unification in combinations of collapse-free regular theories
- Weighted systems of equations
- Learning from Łukasiewicz and Meredith: investigations into proof structures
- A denotational semantics and dataflow construction for logic programs
- A theory of observables for logic programs
- Essential unifiers
- Title not available (Why is that?)
- Unification, weak unification, upper bound, lower bound, and generalization problems
- Substitution, Complementarity, and Stability
- A New Algorithm for Computing Least Generalization of a Set of Atoms
- Compositionality properties of SLD-derivations
- Reduction rules for resolution-based systems
- Short story of the term “algebraic analysis”
- The model evolution calculus as a first-order DPLL method
- Investigations into proof structures
- Weighted graphs: A tool for studying the halting problem and time complexity in term rewriting systems and logic programming
- Finite limits and anti-unification in substitution categories
- On complexity of the anti-unification problem
- On the membership problem for finite automata over symmetric groups
- Title not available (Why is that?)
- A rewrite-based type discipline for a subset of computer algebra
- Automated inferencing
- A sound and complete procedure for a general logic program in non-floundering derivations with respect to the 3-valued stable model semantics
- A Kleene Theorem for Forest Languages
This page was built for publication: Properties of substitutions and unifications
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1074342)
