unify 0.1.6

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

Unify

An implementation of Ruzicka und Privara's algorithm of logical unification for dart and flutter.

This algorithm is an optimization of the algorithm developped by Corbin und Bidoit, which itself is based on Robinson's well known algorithmus. The latter is availlable as 'package:unification'.

Robinson's algorithm is inefficient if the same subterm is given in several locations of a term tree, leading to unnecessarily repeated calculations. Ruzicka und Privara's algorithm takes the structure of terms into account by using directed acyclic graphs instead of the original term trees to avoid unnecessary calculations.

Ideally, in this reduced DAG all equal subterms are represented by one identical subgraph, i.e. one and the same term object.

Additionally, the implementation uses imperativ style leading to manipulation of the input.

Last but not least, the occurs check is executed 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 complex tasks!

Example:

 import 'package:unify/unify.dart';

void main() {
  
// Clause 1
  var term1 = t(1, 1, [
    v(1, 2),
    v(1, 2),
  ]);
  // Clause 2
  var term2 = t(2, 1, [
    v(2, 2),
    t(2, 3, [
      v(2, 4), // circularity: v(2, 2)
    ]),
  ]);

  // Always use different numbers for differents clauses!
  // Clause 3
  var term3 = t(3, 1, [
    v(3, 3),
    v(3, 2),
    v(3, 2),
    v(3, 3),
    v(3, 4),
    v(3, 4),
  ]);
  // Clause 4
  var term4 = t(4, 1, [
    v(4, 6),
    v(4, 2),
    t(4, 3, [
      v(4, 4),
    ]),
    v(4, 5),
    v(4, 2),
    v(4, 6),
  ]);

  // unification modifies terms!
  // find substitutions 
  print('unifiable: ' + mgu(term1, term2).toString());
  // print unified (substitutions found)
  print('term1    : ' + term1.toString());
  print('term2    : ' + term2.toString());
  // print simplified (substitutions materialized)
  print('term1    : ' + term1.substitute.toString());
  print('term2    : ' + term2.substitute.toString());
}