%solve

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

Example

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

%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%sort plus {_ nat} {_ nat} {_ nat} %.
%term pz plus z N N %.
%term ps %pi (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 %.

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

%define six nat s (s four) %.
%define deriv2 (plus four (s (s z)) six) ps (ps deriv) %.

See also

• Solve Declaration (guide §5.24)