Properties of substitutions and unifications

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

scientific article; zbMATH DE number 3774914 (Why is no real title available?)
scientific article; zbMATH DE number 3413831 (Why is no real title available?)
A Machine-Oriented Logic Based on the Resolution Principle
An Efficient Unification Algorithm
Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
Linear unification
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
On equational theories, unification, and (un)decidability
Determinisation of Relational Substitutions in Ordered Categories with Domain
Semantic models for concurrent logic languages
Improving precision of type analysis using non-discriminative union
A new algorithm for computing least generalization of a set of atoms
Multi-valued logic programming semantics An algebraic approach
scientific article; zbMATH DE number 1463151 (Why is no real title available?)
Implication of clauses is undecidable
Specialisation of Prolog and FCP programs using abstract interpretation
A non-ground realization of the stable and well-founded semantics
On the cardinality computation problem for regular languages over symmetric groups
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
Detecting non-provable goals
Unification in a combination of arbitrary disjoint equational theories
A compositional semantics for logic programs
Epsilon-invariant substitutions and indefinite descriptions
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
Compositional confluence criteria
scientific article; zbMATH DE number 3858458 (Why is no real title available?)
Unification, weak unification, upper bound, lower bound, and generalization problems
Substitution, Complementarity, and Stability
Compositionality properties of SLD-derivations
Reduction rules for resolution-based systems
Short story of the term “algebraic analysis”
Weighted graphs: A tool for studying the halting problem and time complexity in term rewriting systems and logic programming
The model evolution calculus as a first-order DPLL method
Investigations into proof structures
Finite limits and anti-unification in substitution categories
On the membership problem for finite automata over symmetric groups
On complexity of the anti-unification problem
scientific article; zbMATH DE number 177828 (Why is no real title available?)
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)