%------------------------------------------------------------------------------
tff(human_type,type, human: $tType ).
tff(cat_type,type, cat: $tType ).
tff(jon_decl,type, jon: human ).
tff(garfield_decl,type, garfield: cat ).
tff(arlene_decl,type, arlene: cat ).
tff(nermal_decl,type, nermal: cat ).
tff(loves_decl,type, loves: cat > cat ).
tff(owns_decl,type, owns: ( human * cat ) > $o ).
tff(only_jon,axiom, ! [H: human] : H = jon ).
tff(only_garfield_and_arlene_and_nermal,axiom,
! [C: cat] :
( C = garfield | C = arlene | C = nermal ) ).
tff(distinct_cats,axiom,
( garfield != arlene & arlene != nermal
& nermal != garfield ) ).
tff(jon_owns_garfield_not_arlene,axiom,
( owns(jon,garfield) & ~ owns(jon,arlene) ) ).
tff(all_cats_love_garfield,axiom,
! [C: cat] : ( loves(C) = garfield ) ).
tff(jon_owns_garfields_lovers,conjecture,
! [C: cat] :
( ( loves(C) = garfield & C != arlene )
=> owns(jon,C) ) ).
%------------------------------------------------------------------------------
|
%------------------------------------------------------------------------------
tff(human_type,type, human: $tType ).
tff(cat_type,type, cat: $tType ).
tff(jon_decl,type, jon: human ).
tff(garfield_decl,type, garfield: cat ).
tff(arlene_decl,type, arlene: cat ).
tff(nermal_decl,type, nermal: cat ).
tff(loves_decl,type, loves: cat > cat ).
tff(owns_decl,type, owns: ( human * cat ) > $o ).
%----Types of the domain elements
tff(d_jon_decl,type, d_jon: human ).
tff(d_garfield_decl,type, d_garfield: cat ).
tff(d_arlene_decl,type, d_arlene: cat ).
tff(d_nermal_decl,type, d_nermal: cat ).
tff(garfield,interpretation,
%----The human domain elements are {d_jon}
( ( ! [DH: human] : ( DH = d_jon )
%----The cat domain elements are {d_garfield,d_arlene,d_nermal}
& ! [DC: cat]:
( DC = d_garfield | DC = d_arlene | DC = d_nermal )
& $distinct(d_garfield,d_arlene,d_nermal) )
%----Interpret functions
& ( jon = d_jon
& garfield = d_garfield
& arlene = d_arlene
& nermal = d_nermal
& loves(d_garfield) = d_garfield
& loves(d_arlene) = d_garfield
& loves(d_nermal) = d_garfield )
%----Interpret predicates
& ( owns(d_jon,d_garfield)
& ~ owns(d_jon,d_arlene)
& ~ owns(d_jon,d_nermal) ) ) ).
%------------------------------------------------------------------------------
|
