Typed 1st Order Logic
Typed first-order logic (also called many sorted logic) extends untyped first-order logic by
adding a finite number of distinct types.
Predicates and functors are declared with type signatures than specify the types of the arguments
and the return type, and variables are given types in their quantification.
The Language of Typed 1st order logic
A typed 1st order language consists of four sets of symbols:
- V is a set of variables (for our purposes, infinite)
- F is a set of functors, each of which has an arity.
The arity specifies the number of arguments they take (see below).
Functors of arity 0 are constants.
- P is a set of predicate symbols, each of which has an arity.
Predicate symbols of arity 0 are propositions.
- T is a set of type symbols.
Prolog syntax is used here: variables start with upper case alphbetic, and functors, predicate,
and type symbols start with lower case alphabetic.
When referring directly to a functor or predicate symbol, its arity is given after a ,
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