unify 0.1.4

An implementation of logical unification for dart and flutter based on the algorithm by Ruzicka und Privara.

Unify

A library providing an implementation of logical unification for dart and flutter based on the algorithm by Ruzicka und Privara.

This algorithm is an optimization of the algorithm by Corbin und Bidoit, which itself is based on Robinsons algorithmus.

Robinsons algorithm is inefficient if a subterm contained in many locations, because the algorithm does not take into account the structure of the to be unified terms. This leads to unnecessary calculations that are avoided by Ruzicka und Privara's algorithm by using directed acyclic graphs instead of the original term trees.

Ideally, in this reduced DAG all equal subterm are represented Teilterme by one identical subgraph.

Additionally, the occurcheck is not executed in each substitution but only after the actual unification as search for cylces in the resulting DAG.

Getting started

Add the dependency to your pubspec.yaml file:

dependencies:
  unify: #latest version

Add the import statement to your source files:

 import 'package:unify/unify.dart';

Or, give it a try and run the example:

dart ./example/main.dart 

Modify the example to test more less simple tasks!

Example:

 import 'package:unify/unify.dart';

void main() {
  

  // occurs check positive:

  var term1 = t(1, 1, [
    v(1, 2),
    v(1, 2),
  ]);

  //
  var term2 = t(2, 1, [
    v(2, 2),
    t(2, 3, [
      v(2, 2),
    ]),
  ]);

  //
  print('\nterm1      > ' + term1.toString());
  print('\nterm2      > ' + term2.toString());
  
  bool res = mgu(term1, term2);
  
  print('\nunifiable  > ' + res.toString());
  print('\nterm1      > ' + term1.toString());
  print('\nterm2      > ' + term2.toString());

}

Read more about unification in logic on Wikipedia.