%solve
From The Twelf Project
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.
[edit] 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.5R3, Aug 30, 2005 (%trustme)%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
[edit] See also
- Solve Declaration in the User's Guide
