tff(garfield_domain,interpretation-domains,
( ! [H: human] : ? [DH: d_human] : H = d2human(DH)
& ! [DH: d_human] : ( DH = d_jon )
& ! [DH1: d_human,DH2: d_human] : ( d2human(DH1) = d2human(DH2) => DH1 = DH2 )
& ! [C: cat] : ? [DC: d_cat] : C = d2cat(DC)
& ! [DC: d_cat]: ( DC = d_garfield | DC = d_arlene | DC = d_nermal )
& $distinct(d_garfield,d_arlene,d_nermal)
& ! [DC1: d_cat,DC2: d_cat] : ( d2cat(DC1) = d2cat(DC2) => DC1 = DC2 ) ) ).
tff(garfield_mapping,interpretation-mappings,
( jon = d2human(d_jon)
& garfield = d2cat(d_garfield)
& arlene = d2cat(d_arlene)
& nermal = d2cat(d_nermal)
& loves(d2cat(d_garfield)) = d2cat(d_garfield)
& loves(d2cat(d_arlene)) = d2cat(d_garfield)
& loves(d2cat(d_nermal)) = d2cat(d_garfield)
& ( owns(d2human(d_jon),d2cat(d_garfield))
& ~ owns(d2human(d_jon),d2cat(d_arlene))
& ~ owns(d2human(d_jon),d2cat(d_nermal)) ) ) ).
tff(garfield_domain_human,interpretation-domains(human,d_human),
! [DH: human] : ( DH = d_jon ) ).
tff(garfield_domain_cat,interpretation-domains(cat,d_cat),
( ! [DC: cat]:
( DC = d_garfield | DC = d_arlene | DC = d_nermal )
& $distinct(d_garfield,d_arlene,d_nermal) ) ).
tff(garfield_mapping_jon,interpretation-mappings(jon,d_human),
jon = d_jon ).
tff(garfield_mapping_garfield,interpretation-mappings(garfied,d_cat),
garfield = d_garfield ).
tff(garfield_mapping_arlene,interpretation-mappings(arlene,d_cat),
arlene = d_arlene ).
tff(garfield_mapping_nermal,interpretation-mappings(nermal,d_cat),
nermal = d_nermal ).
tff(garfield_mapping_loves,interpretation-mappings(loves,d_cat),
( loves(d_garfield) = d_garfield
& loves(d_arlene) = d_garfield
& loves(d_nermal) = d_garfield ) ).
tff(garfield_mapping_owns,interpretation-mappings(owns,$o),
( owns(d_jon,d2cat(d_garfield))
& ~ owns(d_jon,d_arlene)
& ~ owns(d_jon,d_nermal) ) ).
tff(garfield_mapping,interpretation-mappings,
( jon = d2human(d_jon)
& garfield = d2cat(d_garfield)
& arlene = d2cat(d_arlene)
& nermal = d2cat(d_nermal)
& loves(d2cat(d_garfield)) = d2cat(d_garfield)
& loves(d2cat(d_arlene)) = d2cat(d_garfield)
& loves(d2cat(d_nermal)) = d2cat(d_garfield)
& ( owns(d2human(d_jon),d2cat(d_garfield))
& ~ owns(d2human(d_jon),d2cat(d_arlene))
& ~ owns(d2human(d_jon),d2cat(d_nermal)) ) ) ).
tff(garfield_mapping_jon,interpretation-mappings,
( jon = d2human(d_jon)
& garfield = d2cat(d_garfield)
& arlene = d2cat(d_arlene)
& nermal = d2cat(d_nermal)
& ! [DC: d_cat] : ( loves(d2cat(DC)) = d2cat(d_garfield) )
& owns(d2human(d_jon),d2cat(d_garfield))
& ~ owns(d2human(d_jon),d2cat(d_arlene))
& ~ owns(d2human(d_jon),d2cat(d_nermal)) ) ).
| Jon Owns Garfield's Lovers | Finite Countermodel | |
|---|---|---|
%------------------------------------------------------------------------------
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 domains
tff(d_human_type,type, d_human: $tType ).
tff(d_cat_type,type, d_cat: $tType ).
%----Types of the domain elements
tff(d_jon_decl,type, d_jon: d_human ).
tff(d_garfield_decl,type, d_garfield: d_cat ).
tff(d_arlene_decl,type, d_arlene: d_cat ).
tff(d_nermal_decl,type, d_nermal: d_cat ).
%----Types of the promotion functions
tff(d2human_decl,type, d2human: d_human > human ).
tff(d2cat_decl,type, d2cat: d_cat > cat ).
tff(garfield,interpretation,
%----The domain for human is d_human, with elements {d_jon}
( ! [H: human] : ? [DH: d_human] : H = d2human(DH)
& ! [DH: d_human] : ( DH = d_jon )
%----The type-promoter is a bijection
& ! [DH1: d_human,DH2: d_human] :
( d2human(DH1) = d2human(DH2) => DH1 = DH2 )
%----The domain for cat is d_cat, with distinct elements
%----{d_garfield,d_arlene,d_nermal}
& ! [C: cat] : ? [DC: d_cat] : C = d2cat(DC)
& ! [DC: d_cat]:
( DC = d_garfield | DC = d_arlene | DC = d_nermal )
& $distinct(d_garfield,d_arlene,d_nermal)
& ! [DC1: d_cat,DC2: d_cat] :
( d2cat(DC1) = d2cat(DC2) => DC1 = DC2 )
%----Interpret terms via the type-promoted domain
& jon = d2human(d_jon)
& garfield = d2cat(d_garfield)
& arlene = d2cat(d_arlene)
& nermal = d2cat(d_nermal)
& loves(d2cat(d_garfield)) = d2cat(d_garfield)
& loves(d2cat(d_arlene)) = d2cat(d_garfield)
& loves(d2cat(d_nermal)) = d2cat(d_garfield)
%----Interpret atoms as true or false
& owns(d2human(d_jon),d2cat(d_garfield))
& ~ owns(d2human(d_jon),d2cat(d_arlene))
& ~ owns(d2human(d_jon),d2cat(d_nermal)) ) ).
%------------------------------------------------------------------------------
|
%------------------------------------------------------------------------------
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 domains
tff(d_human_type,type, d_human: $tType ).
tff(d_cat_type,type, d_cat: $tType ).
%----Types of the domain elements
tff(d_jon_decl,type, d_jon: d_human ).
tff(d_garfield_decl,type, d_garfield: d_cat ).
tff(d_arlene_decl,type, d_arlene: d_cat ).
tff(d_nermal_decl,type, d_nermal: d_cat ).
%----Types of the promotion functions
tff(d2human_decl,type, d2human: d_human > human ).
tff(d2cat_decl,type, d2cat: d_cat > cat ).
tff(garfield_domain,interpretation-domains,
%----The domain for human is d_human, with elements {d_jon}
( ! [H: human] : ? [DH: d_human] : H = d2human(DH)
& ! [DH: d_human] : ( DH = d_jon )
%----The type-promoter is a bijection
& ! [DH1: d_human,DH2: d_human] :
( d2human(DH1) = d2human(DH2) => DH1 = DH2 )
%----The domain for cat is d_cat, with distinct elements
%----{d_garfield,d_arlene,d_nermal}
& ! [C: cat] : ? [DC: d_cat] : C = d2cat(DC)
& ! [DC: d_cat]:
( DC = d_garfield | DC = d_arlene | DC = d_nermal )
& $distinct(d_garfield,d_arlene,d_nermal)
& ! [DC1: d_cat,DC2: d_cat] :
( d2cat(DC1) = d2cat(DC2) => DC1 = DC2 ) ) ).
tff(garfield_mapping,interpretation-mappings,
%----Interpret terms via the type-promoted domain
( jon = d2human(d_jon)
& garfield = d2cat(d_garfield)
& arlene = d2cat(d_arlene)
& nermal = d2cat(d_nermal)
& loves(d2cat(d_garfield)) = d2cat(d_garfield)
& loves(d2cat(d_arlene)) = d2cat(d_garfield)
& loves(d2cat(d_nermal)) = d2cat(d_garfield)
%----Interpret atoms as true or false
& ( owns(d2human(d_jon),d2cat(d_garfield))
& ~ owns(d2human(d_jon),d2cat(d_arlene))
& ~ owns(d2human(d_jon),d2cat(d_nermal)) ) ) ).
%------------------------------------------------------------------------------
|
| Jon Owns Garfield's Lovers | Finite Countermodel - Fine Grained | |
|---|---|---|
%------------------------------------------------------------------------------
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 domains
tff(d_human_type,type, d_human: $tType ).
tff(d_cat_type,type, d_cat: $tType ).
%----Types of the domain elements
tff(d_jon_decl,type, d_jon: d_human ).
tff(d_garfield_decl,type, d_garfield: d_cat ).
tff(d_arlene_decl,type, d_arlene: d_cat ).
tff(d_nermal_decl,type, d_nermal: d_cat ).
%----Types of the promotion functions
tff(d2human_decl,type, d2human: d_human > human ).
tff(d2cat_decl,type, d2cat: d_cat > cat ).
tff(garfield,interpretation,
%----The domain for human is d_human, with elements {d_jon}
( ! [H: human] : ? [DH: d_human] : H = d2human(DH)
& ! [DH: d_human] : ( DH = d_jon )
%----The type-promoter is a bijection
& ! [DH1: d_human,DH2: d_human] :
( d2human(DH1) = d2human(DH2) => DH1 = DH2 )
%----The domain for cat is d_cat, with distinct elements
%----{d_garfield,d_arlene,d_nermal}
& ! [C: cat] : ? [DC: d_cat] : C = d2cat(DC)
& ! [DC: d_cat]:
( DC = d_garfield | DC = d_arlene | DC = d_nermal )
& $distinct(d_garfield,d_arlene,d_nermal)
& ! [DC1: d_cat,DC2: d_cat] :
( d2cat(DC1) = d2cat(DC2) => DC1 = DC2 )
%----Interpret terms via the type-promoted domain
& jon = d2human(d_jon)
& garfield = d2cat(d_garfield)
& arlene = d2cat(d_arlene)
& nermal = d2cat(d_nermal)
& loves(d2cat(d_garfield)) = d2cat(d_garfield)
& loves(d2cat(d_arlene)) = d2cat(d_garfield)
& loves(d2cat(d_nermal)) = d2cat(d_garfield)
%----Interpret atoms as true or false
& owns(d2human(d_jon),d2cat(d_garfield))
& ~ owns(d2human(d_jon),d2cat(d_arlene))
& ~ owns(d2human(d_jon),d2cat(d_nermal)) ) ).
%------------------------------------------------------------------------------
|
%------------------------------------------------------------------------------
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 domains
tff(d_human_type,type, d_human: $tType ).
tff(d_cat_type,type, d_cat: $tType ).
%----Types of the domain elements
tff(d_jon_decl,type, d_jon: d_human ).
tff(d_garfield_decl,type, d_garfield: d_cat ).
tff(d_arlene_decl,type, d_arlene: d_cat ).
tff(d_nermal_decl,type, d_nermal: d_cat ).
%----Types of the promotion functions
tff(d2human_decl,type, d2human: d_human > human ).
tff(d2cat_decl,type, d2cat: d_cat > cat ).
tff(garfield_domain_human,interpretation-domains(human,d_human),
%----The domain for human is d_human, with elements {d_jon}
( ! [H: human] : ? [DH: d_human] : H = d2human(DH)
& ! [DH: d_human] : ( DH = d_jon )
%----The type-promoter is a bijection
& ! [DH1: d_human,DH2: d_human] :
( d2human(DH1) = d2human(DH2) => DH1 = DH2 ) ) ).
tff(garfield_domain_cat,interpretation-domains(cat,d_cat),
%----The domain for cat is d_cat, with distinct elements
%----{d_garfield,d_arlene,d_nermal}
( ! [C: cat] : ? [DC: d_cat] : C = d2cat(DC)
& ! [DC: d_cat]:
( DC = d_garfield | DC = d_arlene | DC = d_nermal )
& $distinct(d_garfield,d_arlene,d_nermal)
& ! [DC1: d_cat,DC2: d_cat] :
( d2cat(DC1) = d2cat(DC2) => DC1 = DC2 ) ) ).
tff(garfield_mapping_jon,interpretation-mappings(jon,d_human),
jon = d2human(d_jon) ).
tff(garfield_mapping_garfield,interpretation-mappings(garfied,d_cat),
garfield = d2cat(d_garfield) ).
tff(garfield_mapping_arlene,interpretation-mappings(arlene,d_cat),
arlene = d2cat(d_arlene) ).
tff(garfield_mapping_nermal,interpretation-mappings(nermal,d_cat),
nermal = d2cat(d_nermal) ).
tff(garfield_mapping_loves,interpretation-mappings(loves,d_cat),
( loves(d2cat(d_garfield)) = d2cat(d_garfield)
& loves(d2cat(d_arlene)) = d2cat(d_garfield)
& loves(d2cat(d_nermal)) = d2cat(d_garfield) ) ).
tff(garfield_mapping_owns,interpretation-mappings(owns,$o),
( owns(d2human(d_jon),d2cat(d_garfield))
& ~ owns(d2human(d_jon),d2cat(d_arlene))
& ~ owns(d2human(d_jon),d2cat(d_nermal)) ) ).
%------------------------------------------------------------------------------
|
| Jon Owns Garfield's Lovers | Compacted | |
|---|---|---|
%------------------------------------------------------------------------------
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 domains
tff(d_human_type,type, d_human: $tType ).
tff(d_cat_type,type, d_cat: $tType ).
%----Types of the domain elements
tff(d_jon_decl,type, d_jon: d_human ).
tff(d_garfield_decl,type, d_garfield: d_cat ).
tff(d_arlene_decl,type, d_arlene: d_cat ).
tff(d_nermal_decl,type, d_nermal: d_cat ).
%----Types of the promotion functions
tff(d2human_decl,type, d2human: d_human > human ).
tff(d2cat_decl,type, d2cat: d_cat > cat ).
tff(garfield_domain,interpretation-domains,
%----The domain for human is d_human, with elements {d_jon}
( ! [H: human] : ? [DH: d_human] : H = d2human(DH)
& ! [DH: d_human] : ( DH = d_jon )
%----The type-promoter is a bijection
& ! [DH1: d_human,DH2: d_human] :
( d2human(DH1) = d2human(DH2) => DH1 = DH2 )
%----The domain for cat is d_cat, with distinct elements
%----{d_garfield,d_arlene,d_nermal}
& ! [C: cat] : ? [DC: d_cat] : C = d2cat(DC)
& ! [DC: d_cat]:
( DC = d_garfield | DC = d_arlene | DC = d_nermal )
& $distinct(d_garfield,d_arlene,d_nermal)
& ! [DC1: d_cat,DC2: d_cat] :
( d2cat(DC1) = d2cat(DC2) => DC1 = DC2 ) ) ).
tff(garfield_mapping,interpretation-mappings,
%----Interpret terms via the type-promoted domain
( jon = d2human(d_jon)
& garfield = d2cat(d_garfield)
& arlene = d2cat(d_arlene)
& nermal = d2cat(d_nermal)
& loves(d2cat(d_garfield)) = d2cat(d_garfield)
& loves(d2cat(d_arlene)) = d2cat(d_garfield)
& loves(d2cat(d_nermal)) = d2cat(d_garfield)
%----Interpret atoms as true or false
& ( owns(d2human(d_jon),d2cat(d_garfield))
& ~ owns(d2human(d_jon),d2cat(d_arlene))
& ~ owns(d2human(d_jon),d2cat(d_nermal)) ) ) ).
%------------------------------------------------------------------------------
|
%------------------------------------------------------------------------------
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 domains
tff(d_human_type,type, d_human: $tType ).
tff(d_cat_type,type, d_cat: $tType ).
%----Types of the domain elements
tff(d_jon_decl,type, d_jon: d_human ).
tff(d_garfield_decl,type, d_garfield: d_cat ).
tff(d_arlene_decl,type, d_arlene: d_cat ).
tff(d_nermal_decl,type, d_nermal: d_cat ).
%----Types of the promotion functions
tff(d2human_decl,type, d2human: d_human > human ).
tff(d2cat_decl,type, d2cat: d_cat > cat ).
tff(garfield_domain,interpretation-domains,
%----The domain for human is d_human, with elements {d_jon}
( ! [H: human] : ? [DH: d_human] : H = d2human(DH)
& ! [DH: d_human] : ( DH = d_jon )
%----The type-promoter is a bijection
& ! [DH1: d_human,DH2: d_human] :
( d2human(DH1) = d2human(DH2) => DH1 = DH2 )
%----The domain for cat is d_cat, with distinct elements
%----{d_garfield,d_arlene,d_nermal}
& ! [C: cat] : ? [DC: d_cat] : C = d2cat(DC)
& ! [DC: d_cat]:
( DC = d_garfield | DC = d_arlene | DC = d_nermal )
& $distinct(d_garfield,d_arlene,d_nermal)
& ! [DC1: d_cat,DC2: d_cat] :
( d2cat(DC1) = d2cat(DC2) => DC1 = DC2 ) ) ).
tff(garfield_mapping,interpretation-mappings,
%----Interpret terms via the type-promoted domain
( jon = d2human(d_jon)
& garfield = d2cat(d_garfield)
& arlene = d2cat(d_arlene)
& nermal = d2cat(d_nermal)
& ! [DC: d_cat] : ( loves(d2cat(DC)) = d2cat(d_garfield) )
%----Interpret atoms as true or false
& ( owns(d2human(d_jon),d2cat(d_garfield))
& ~ owns(d2human(d_jon),d2cat(d_arlene))
& ~ owns(d2human(d_jon),d2cat(d_nermal)) ) ) ).
%------------------------------------------------------------------------------
|