%solve

From The Twelf Project
Jump to: navigation, search

A %solve declaration specifies a type and then uses Twelf's logic programming engine to search for an term with that type. It is different from %query, both because it can only cause Twelf to search for the first proof it can find and because it can add the result of the search to the Twelf signature.

Example

We can define natural numbers with addition in the standard manner:

nat : type.
z : nat.
s : nat -> nat.

plus : nat -> nat -> nat -> type.
pz : plus z N N.
ps : plus N1 N2 N3 -> plus (s N1) N2 (s N3).

Then we can use %solve and %define to insert the result of adding two and two to the signature as four, and the derivation itself to the signature as deriv.

%define four = N
%solve deriv : plus (s (s z)) (s (s z)) N.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%solve plus (s (s z)) (s (s z)) N. OK four : nat = s (s (s (s z))). deriv : plus (s (s z)) (s (s z)) (s (s (s (s z)))) = ps (ps pz).

%% OK %%

We can then use five and deriv as a defined constants for the rest of the program:

six : nat = s (s four).
deriv2 : plus four (s (s z)) six = ps (ps deriv).
See Twelf's output

See also