unification 0.1.3 copy "unification: ^0.1.3" to clipboard
unification: ^0.1.3 copied to clipboard

outdated

Unification is an implementation of logical first-order unification. It follows Robinson's algorithm, and uses trampolining to avoid stack size limitation issues.

unification #

Unification is an implementation of logical first-order unification.

A first-order unification procedure unify is given by this library. It can be applied on two terms of type Termtype that are also given by the library.

The solution of a unification problem is a substitution, that is, a mapping assigning a symbolic value to each variable of the problem's expressions.

The unification procedure reports unsolvability for a given problem or computes the complete and minimal substitution set containing the most general unifier. This is a set covering all solutions containing no redundant members.

Example: #

import "package:tailcalls/tailcalls.dart";
import "package:unification/unification.dart";

var test = unify(
      new List()
        ..add(
          new Tupl(
            new Term("b0", [new Term("b1", []),new Term("b2", [])]),
            new Term("b0", [new Term("b1", []),new Term("b2", [])]),
          ),
        ),
    ).result();
var mgu = test;
print(mgu.toString());

Read more about unification in logic on Wikipedia.

1
likes
0
pub points
0%
popularity

Publisher

verified publisherwelopment.com

Unification is an implementation of logical first-order unification. It follows Robinson's algorithm, and uses trampolining to avoid stack size limitation issues.

Repository (GitHub)
View/report issues

License

unknown (LICENSE)

Dependencies

tailcalls

More

Packages that depend on unification