The goal of this document is to:
tff(a_type,type,a:animal).
tff(b_type,type,b:integer).
tff(has_4_legs_type,type,has_4_legs: animal > $oType).
tff(some_integer_animal,axiom,a = b).
tff(a_has_4_legs,axiom,has_4_legs(a)).
tff(b_has_4_legs,plain,has_4_legs(b),inferred(paramodulation ...
To overcome this problem would require either multiple equality symbols
or polymorphic equality (see below).
a:$iType; f:fruit; ifun: $iType -> $iType; fruitfun: fruit -> fruit; a = f ifun(f) fruitfun(a)
tff(cons_type,type,
cons: (int * list) > list ).
tff(is_empty_type,type,
isEmpty:list > $oType ).
tff(list_not_empty,axiom,
! [X:int,Xs:list] : ~isEmpty(cons(X,Xs)) ).
tff(f_type,type,
f: (t1 * ... * tn) > tf ). is translated into:
fof(f_type,axiom,
! [X1,...,Xn] :
( ( t1(X1)
& ...
& t2(Xn) )
=> tf(f(X1,...,Xn)) ) ).
! [X1:t1,...,Xn:tn] : p(X1,...,Xn)is translated into:
! [X1,...,Xn] :
( ( t1(X1)
& ...
& tn(Xn) )
=> p(X1,...,Xn) )
? [X1:t1,...,Xn:tn] : p(X1,...,Xn)is translated into:
? [X1,...,Xn] :
( t1(X1)
& ...
& tn(Xn)
& p(X1,...,Xn) )
Theorem provers: TODO. Reference: SPASS and soft typing.
Model finders have an easier task to find typed models, as long as the domains of the separate types are as most as large as the domain of the untyped version of the problem. This is the case for the first proposal, but definitely not for the second.
! [X:(human & male)] : ~ has_ovary(X)
? [Y:(republican | democrat)] : president(Y)
! [M : matrix(4)] : M = M
These are translated as
! [X] : ((human(X) & male(X)) => ~ has_ovary(X))
? [Y] : ((republican(Y) | democrat(Y)) & president(Y))
! [M] : (matrix(X,4) => M = M)
Can/should this be integrated?