Thanks Boris!
Here’s the order sorted logic from the Eco Logic book. The book describes it all in psuedocode which is basically just IF-THEN-ELSE rules - easy tranlsation to Prolog.
%-*-mode:prolog-*-
%%%
%%% Eco-Logic: Logic-Based Approaches to Ecological Modelling.
%%% Robertson et al.
%%%
%%% Chapter 4 An Order Sorted Logic
%%%
%%%
%%% [-'../../misc/Eco_Logic.code/chap4/order_sorted_logic'].
%%%
%%%
%%% If things are not defined then they should fail.
%%% Example : no sort_term predicates defined should fail.
%%%
:-set_prolog_flag(unknown, fail).
:-op(950, xfx, #).
:-op(900, xfx, <-).
:-op(900, xfx, <=).
:-op(700, xfx, in).
:-op(500, yfx, and).
:-op(500, yfx, or).
%%%
%%% Obj in Sort
%%%
%%% Object is a member of Sort.
%%%
Obj in Sort :-
var(Obj),
var(Sort),
throw(error(domain_error(in/2, Obj, Sort))).
Obj in Set :-
member(Obj, Set).
Obj in Sort :-
subobj(Sort, Obj).
Obj in Sort :-
subsort(Sort, SubSort),
Obj in SubSort.
Obj in Sort :-
sort_term(Sort, Obj, Consts),
satisfiable_constraints(Consts).
Obj in srelation(Relation) :-
sort_relation(Relation, Consts),
satisfiable_constraints(Consts).
Obj in Sort :-
sort_test(Sort, Obj, Test),
call(Test).
Obj in Sort1 and Sort2 :-
Obj in Sort1,
Obj in Sort2.
Obj in Sort1 or Sort2 :-
Obj in Sort1;
Obj in Sort2.
Obj in inv(Sort) :-
\+ Obj in Sort.
%%%
%%% satisfiable_constraints(+Consts)
%%%
%%% All of the elements of the list of constraints
%%% Consts are satisfiable.
%%%
satisfiable_constraints([]).
satisfiable_constraints([Obj in Sort|Rest]) :-
Obj in Sort,
satisfiable_constraints(Rest).
%%%
%%% solve(+Term, ?Result)
%%%
%%% The interpreter
%%%
solve(Term, Result) :-
term_class(primitive, Term),
!,
Result = Term.
solve((Obj in Sort), Obj) :-
!,
Obj in Sort.
solve((A and B), (RA and RB)) :-
!,
solve(A, RA),
solve(B, RB).
solve((A or _), RA) :-
solve(A, RA).
solve((_ or B), RB) :-
!,
solve(B, RB).
solve([H|T], [R|Rest]) :-
!,
solve(H, R),
solve(T, Rest).
solve(((Ins, Outs)#Tm), Result) :-
!,
satisfiable_constraints(Ins),
solve(Tm, Result),
satisfiable_constraints(Outs).
solve(Term, Result) :-
meta_fun(Term, Result, Call),
!,
call(Call).
solve(Term, Result) :-
meta_pred(Term, Call),
!,
call(Call),
Term = Result.
solve(Term, Result) :-
% nonvar(Term),
compound(Term),
standardise_term(Term, ETerm),
(term_class(function, ETerm), !, osl_eval(ETerm, Result)
;
term_class(predicate, ETerm), establish(ETerm, Result)).
%%%
%%% solve_list(+L,-S)
%%%
%%% S is the list L where each element is sorted.
%%%
solve_list([], []).
solve_list([H|T], [SH|ST]) :-
solve(H,SH),
solve_list(T,ST).
%%%
%%% standardise_term(+Term, -ETerm)
%%%
%%% The Term in the sorted logic can be standardised to form the term
%%% ETerm with all its arguments fully evaluated.
%%%
standardise_term(Term, ETerm) :-
Term =..[Functor|Args],
solve_list(Args, RArgs),
ETerm =.. [Functor|RArgs].
%%%
%%% osl_eval(+Term, -Result)
%%%
%%%
%%%
osl_eval(Term, Result) :-
sys_fun(Term, (Ins,Outs), Result in Sort, Call),
satisfiable_constraints(Ins),
call(Call),
satisfiable_constraints(Outs),
Result in Sort.
osl_eval(Term, Result) :-
term_class(defined_function, Term),
(Ins,Outs)#Term1 <= Body,
standardise_term(Term1, ETerm1),
Term = ETerm1,
satisfiable_constraints(Ins),
solve(Body, Result),
satisfiable_constraints(Outs).
%%%
%%% establish(+Term, -Result)
%%%
%%%
%%%
establish(Term, Result) :-
sys_pred(Term, (Ins, Outs), Call),
satisfiable_constraints(Ins),
call(Call),
satisfiable_constraints(Outs),
Result = Term.
establish(Term, Result) :-
term_class(defined_predicate, Term),
((Ins,Outs)#Term1,
standardise_term(Term1, ETerm1),
Term=ETerm1,
satisfiable_constraints(Ins),
satisfiable_constraints(Outs),
Result=Term
;
(Ins,Outs)#Term1 <- Body,
standardise_term(Term1, ETerm1),
Term=ETerm1,
satisfiable_constraints(Ins),
solve(Body,_),
satisfiable_constraints(Outs),
Result=Term).
%%%
%%% term_class(C, T)
%%%
%%% Term T is of class C.
%%%
term_class(primitive, Term) :-
number(Term),
!.
term_class(primitive, Term) :-
atom(Term),
!.
term_class(primitive, Term) :-
var(Term),
!.
term_class(defined_predicate, Term) :-
def(Term, pred(_,_)),
!.
term_class(defined_function, Term) :-
def(Term, fun(_,_,_)),
!.
term_class(predicate, Term) :-
sys_pred(Term, _, _),
!.
term_class(predicate, Term) :-
term_class(defined_predicate, Term),
!.
term_class(function, Term) :-
sys_fun(Term, _, _, _),
!.
term_class(function, Term) :-
term_class(defined_function, Term).
%%%
%%% Built in sorts
%%%
sort_test(number, N, number(N)).
%%%
%%% Built in system functions.
%%%
sys_fun(A*B, ([A in number, B in number], []), C in number, C is A*B).
sys_fun(A-B, ([A in number, B in number], []), C in number, C is A-B).
sys_fun(A/B, ([A in number, B in number], []), C in number, C is A/B).
sys_fun(A+B, ([A in number, B in number], []), C in number, C is A+B).
%%%
%%% sum_elements(+Lst, +Acc, -Sum)
%%%
%%% The sum of the elements of Lst plus Acc is Sum.
%%%
sum_elements([], Sum, Sum).
sum_elements([H|T], Acc0, Sum) :-
Acc1 is Acc0 + H,
sum_elements(T, Acc1, Sum).
%%%
%%% sum_elements(+Lst, -Sum)
%%%
%%% The summation of all of the elements of Lst is Sum.
%%%
sum_elements(Lst, Sum) :-
sum_elements(Lst, 0, Sum).
sys_fun(sum(Lst), ([], []), Sum in number, sum_elements(Lst, Sum)).
%%%
%%% Built in system predicates.
%%%
sys_pred(A=B, ([], [A in universal, B in universal]), A=B).
sys_pred(A<B, ([], [A in number, B in number]), A<B).
sys_pred(A=<B, ([], [A in number, B in number]), A=<B).
sys_pred(A=:=B, ([], [A in number, B in number]), A=:=B).
sys_pred(A>=B, ([], [A in number, B in number]), A>=B).
sys_pred(A>B, ([], [A in number, B in number]), A>B).
%%%
%%% Built in meta-functions.
%%%
meta_fun(setof(F), Set, (findall(X, solve(F, X), Bag), sort(Bag, Set))).
meta_fun(bagof(F), Bag, findall(X, solve(F, X), Bag)).
My first attempt at the steamroller last night. It got late so I stopped before I got to the interesting clauses and went to sleep. You get an idea of the sort definitions though.
/*
Wolves, fishes, birds, caterpillars, and snails are animals, and there is at least
one of each kind of animal. Grain is a plant, and there exists at least on such
plant. Every animal is an herbivore or else eats eats all herbivores which are
much smaller than itself. Caterpillars and snails are much smaller than birds, which
in turn are much smaller than fish, and fish are much smaller than wolves.
Caterpillars and snails are herbivores. It is to be shown that there exists an
animal that eats a grain-eating animal.
*/
subsort(universal, animal).
subsort(universal, plant).
subsort(animal, wolf).
subsort(animal, fish).
subsort(animal, bird).
subsort(animal, caterpillar).
subsort(animal, snail).
subsort(grain, plant).
subobj(wolf, w).
subobj(fish, f).
subobj(bird, b).
subobj(caterpillar, c).
subobj(snail, s).
subobj(grain, g).
def(much_smaller_than(X, Y), pred([X in universal, Y in universal], [])).
def(eats(X, Y), pred([X in universal, Y in universal], [])).
([X in caterpillar, Y in bird], []) # much_smaller_than(X, Y).
([X in snail, Y in bird], []) # much_smaller_than(X, Y).
([X in bird, Y in fish], []) # much_smaller_than(X, Y).
([X in fish, Y in wolf], []) # much_smaller_than(X, Y).
([X in wolf], [ Y in inv(fish or grain)]) # eats(X, Y).