, e.g., in blah/2, blah
is the functor or predicate symbol and the arity is 2.
| Example
|
|---|
V = { V : V starts with uppercase }
F = { garfield/0, odie/0, jon/0, owner_of/1 }
P = { hates/2, chased/2 }
T = { cat, dog, pet, human }
|
The type signatures (argument and return types) of constants, functors, and
predicates are declared, and all formulae must respect the type signatures.
The TPTP Typed First-order Form (TFF)
TPTP Typed First-order Form (TFF) formulae are written in tff(...)
annotated formulae.
The TPTP world predefines several types:
- $i - the type of individuals, which can be used as a default
type for terms.
- $o - booleans (the return type for predicates).
- $int, $rat, $real - arithmetic types.
User types are declared to be of the psuedo-type $tType.
All user types, and the type signatures of constants, functors, and predicates,
should be declared before use, in annotated formulae with the role
type (those that are not declared get default type signatures using
$i and $o.
| Example
|
|---|
tff(pet_type,type,pet: $tType ).
tff(cat_type,type,cat: $tType ).
tff(dog_type,type,dog: $tType ).
tff(human_type,type,human: $tType ).
tff(garfield_type,type,garfield: cat ).
tff(odie_type,type,odie: dog ).
tff(jon_type,type,jon: human ).
tff(owner_of_type,type,owner_of: pet > human ).
tff(chased_type,type,chased: ( dog * cat ) > $o ).
tff(hates_type,type,hates: ( human * human ) > $o ).
|
The types of variables are declared in their quantification.
| Example
|
|---|
tff(human_owner,axiom,! [A: pet] : ? [H: human] : H = owner_of(A) ).
|
Equality is adhoc polymorphic over the types, requiring that both arguments
have the same type.
Subtypes are not available (yet), so this is not allowed ...
tff(dog_chase_cat,axiom,
! [C: cat,D: dog] :
( chased(D,C)
=> hates(owner_of(C),owner_of(D)) ) ).
... because it is not known that cats and dogs are pets.
One way to solve this is to use a type-conversion function ...
| Example
|
|---|
tff(cat_to_pet_type,type,cat_to_pet: cat > pet ).
tff(dog_to_pet_type,type,dog_to_pet: dog > pet ).
tff(jon_owns_garfield,axiom,jon = owner_of(cat_to_pet(garfield)) ).
tff(jon_owns_odie,axiom,jon = owner_of(dog_to_pet(odie)) ).
tff(jon_owns_only,axiom,
! [A: pet] :
( jon = owner_of(A)
=> ( A = cat_to_pet(garfield) | A = dog_to_pet(odie) ) ) ).
tff(dog_chase_cat,axiom,
! [C: cat,D: dog] :
( chased(D,C)
=> hates(owner_of(cat_to_pet(C)),owner_of(dog_to_pet(D))) ) ).
|
Translation from English to 1st Order Logic
There is often a direct translation from a problem stated in a natural
language to typed 1st order logic.
In order to make such a translation, it is necessary to:
- Determine the predicates and functors of the 1st order language.
- Objects often correspond to constants
- Relationships that identify a constant often correspond to functors
- Properties and activities often correspond to predicates
- Determine the types that are used.
- Define the necessary types, and declare the signatures of the constants,
functors, and predicates.
- Translate the axioms.
- Make appropriate definitions for the predicates and functors.
- Translate the conjecture.
| Example
|
|---|
|
Every student is enrolled in at least one course.
Every professor teaches at least one course.
Every course has at least one student enrolled.
Every course has at least one professor teaching it.
The coodinator of a course is a professor who is teaching it.
If a student is enrolled in a course then the student is taught by every
professor who teaches the course.
CSC410 is a course.
Michael is a student enrolled in CSC410.
Victor is the coordinator of CSC410.
Therefore, Michael is taught by Victor.
|
Exercises
Convert the following into typed 1st order logic:
- Osama Bin Laden is a dangerous terrorist.
If someone is a dangerous terrorist, then his leader is a dangerous
terrorist.
There are some terrorists who are their own leader.
Therefore, dangerous people care about only themselves, or about no-one
(not even themselves!).
- The depth and time of a SCUBA dive determine the nitrogen absorbed
on the dive.
If the nitrogen absorbed on a SCUBA dive is greater than the limit,
then the outcome of the dive is illness.
Therefore, illness is the only possible bad outcome of a SCUBA dive.
- A capital is a city.
USA is a country.
Every city has crime.
Washington is the capital of the USA.
Every country has a beautiful capital.
Therefore, Washington is beautiful but has crime.
- Iokaste is a parent of Oedipus.
Iokaste is a parent of Polyneikes.
Oedipus is a parent of Polyneikes.
Polyneikes is a parent of Thersandros.
Oedipus is a patricide.
Thersandros is not a patricide.
Therefore, Iokaste is a parent of a patricide that is a parent of
somebody who is not a patricide.
- Wolves, foxes, birds, caterpillars, and snails are animals, and there
are some of each of them. Also there are some grains, and grains are
plants.
Every animal either likes to eat all plants or all animals much smaller
than itself that like to eat some plants.
Caterpillars and snails are much smaller than birds, which are much
smaller than foxes, which in turn are much smaller than wolves.
Wolves do not like to eat foxes or grains, while birds like to eat
caterpillars but not snails.
Caterpillars and snails like to eat some plants.
Therefore, there is an animal that likes to eat a grain eating animal.
Interpretation
Interpretation of typed 1st order formulae requires a slightly more complex
structure than for first-order logic.
An interpretation of a typed 1st order logic consists of three parts:
- D is a set of distinct, non-empty domains, of the interpretation.
There is one domain for each type in T.
- F provides a function for each function symbol, from the arguments'
types' domain elements to the return type domain.
- R provides a function for each predicate symbol, from the arguments'
types' domain elements to the truth values TRUE and
FALSE.
Conversion to Untyped 1st Order Logic
Types first-order logic can be translated to untyped first-order logic.
Each type becomes a new unary predicate in the untyped world.
- A TFF type declaration a_sort: $tType produces a FOF axiom
? [X] : a_sort(X).
This ensures that sorts are inhabited.
- Pairs of TFF sort declarations
one_sort: $tType and two_sort: $tType
produce a FOF axiom
! [X,Y] : ( one_sort(X) & two_sort(Y) ) => X != Y.
This ensures that sorts are pairwise disjoint.
(Note: These axioms are not logically necessary, because a model of the
FOF formulae without these axioms can be used to construct a model of the
TFF formulae, i.e., a formula has a model with disjoint domains iff
it has a model with one domain.
However, for model generation these axioms are useful because they
force terms with different types to be interpreted as different domain
elements, i.e., the domain of the FOF model can be divided into
subdomains for the different sorts.)
- A TFF function type declaration
f: (t_1 *...* t_n) > t_f
produces a FOF axiom
! [X_1,...,X_n] : t_f(X_1,...,X_n).
(It is unnecessary to have an implication with the antecedent checking
the sorts of the arguments X1,...,Xn, because it is impossible
to use incorrectly typed arguments in a well-typed formula.)
- Predicate type declarations are ignored.
- A TFF universally quantified formula
! [X_1:t_1,...,X_n:t_n] : p(X_1,...,X_n)
produces a FOF formula
! [X_1,...,X_n] : ((t_1(X_1) &...& t_n(X_n)) => p(X_1,...,X_n) ).
- A TFF existentially quantified formula
? [X_1:t_1,...,X_n:t_n] : p(X_1,...,X_n)
produces a FOF formula
? [X_1,...,X_n] : (t_1(X_1) &...& t_n(X_n) &
p(X_1,...,X_n)).
Exam Style Questions