Twelf Architecture

?- G.

Proof Engine

M1 =? M2

Unification

X(c) =? Y(d)

...

Z . N

Constraint

Store

Z . N

Z . N

Z . N

...

Undo Stack

Unification Constraint Solver

Previous slide

Next slide

Back to first slide

View graphic version