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: 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 
T = { cat, dog, pet, human }
V = { V : V starts with uppercase }
F = { garfield/0, odie/0, jon/0, owner_of/1 }
P = { hates/2, chased/2 }

The type signatures (argument and return types) of constants, functors, and predicates are declared, and all formulae must respect the type signatures. For example:

Example 
garfield: cat
odie: dog
jon: human
owner_of: pet → human
hates: human * human → boolean
chased: dog * cat → boolean

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:

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.

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. 
T = { student, professor, course }
V = { V : V starts with uppercase }
F = { michael/0, victor/0, csc410/0, coordinator_of/1 }
P = { student/1, professor/1, course/1, enrolled/2, teaches/2, taught_by/2 }

michael: student
victor: professor
csc410: course
coordinator_of: course → professor
enrolled: student * course → boolean
teaches: professor * course → boolean
taught_by: student * professor → boolean

  • Every student is enrolled in at least one course.

    ! [S: student] : ? [C: course] : enrolled(S,C)

  • Every professor teaches at least one course.

    ! [P: professor] : ? [C] : teaches(P,C)

  • Every course has at least one student enrolled.

    ! [C: course] : ? [S: student] : enrolled(S,C)

  • Every course has at least one professor teaching it.

    ! [C: course] : [P: professor] : teaches(P,C)

  • The coodinator of a course is a professor who is teaching it.

    ! [C: course] : ( professor(coordinator_of(C)) & teaches(coordinator_of(C),C) )

  • If a student is enrolled in a course then the student is taught by every professor who teaches the course.

    ! [S: student,C: course] :
      ( enrolled(S,C) => ! [P: professor] : ( teaches(P,C) => taught_by(S,P) ) )

  • CSC410 is a course. In the type declarations

  • Michael is a student enrolled in CSC410.

    enrolled(michael,csc410)

  • Victor is the coordinator of CSC410.

    coordinator_of(csc410) = victor

  • Victor teaches Michael.

    taught_by(michael,victor)

Educational Example

Exercises

Convert the following into typed 1st order logic:

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:

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.

Exam Style Questions