Typed First-order Logic (TFF)
New logic features
- TPTP defined types, user types
- Signatures for predicates and functions, arguments not boolean
- Typed variables, not boolean
Problem
- Axioms
- All humans are created equal.
- John is a human.
- John got an F grade.
- There is some human who got an A grade.
- An A grade is not equal to an F grade.
- Conjecture
- There is a human other than John, who was created equal to John
In logic
- Type information
- human is a type
- grade is a type
- john is a human
- a is a grade
- f is a grade
- grade_of takes one human argument and returns
their grade
- created_equal takes two human arguments
and returns boolean
- Axioms
- ∀ H1:human
∀ H2:human created_equal(H1,H2)
- grade_of(john) = f
- ∃ H:human grade_of(H) = a
- a ≠ f
- Conjecture
- ∃ H:human (H ≠ john ∧ created_equal(H,john))
In TPTP format
- TPTP defined types: $i $o
- User types: Declared of "type" $tType, in annotated formulae with type role
- Predicate and function signatures: Declared in annotated formulae with type role,
arguments not $o
- Variables: Given type in quantification, not $o
- tff annotated formulae have a name (lowercase), a role (axiom,
conjecture, and others), a formula, and end with .
-
tff(human_type,type,human: $tType).
tff(grade_type,type,grade: $tType).
tff(john_decl,type,john: human).
tff(a_decl,type,a: grade).
tff(f_decl,type,f: grade).
tff(grade_of_decl,type,grade_of: human > grade).
tff(created_equal_decl,type,created_equal: (human * human) > $o).
tff(all_created_equal,axiom,
! [H1:human,H2:human] : created_equal(H1,H2) ).
tff(john_got_an_f,axiom,
grade_of(john) = f ).
tff(someone_got_an_a,axiom,
? [H:human] : grade_of(H) = a ).
tff(a_is_not_f,axiom,
a != f ).
tff(there_is_someone_else,conjecture,
? [H:human] :
( H != john
& created_equal(H,john) ) ).
- Check the syntax in
SystemB4TPTP using TPTP4X.
- Check the axioms are satisfiable with Vampire-SAT in
SystemOnTPTP.
- Try prove it using Vampire in
SystemOnTPTP.
- View the derivation using IDV in
SystemOnTSTP.
- Verify the derivation using GDV in
SystemOnTSTP.
Challenge problem
Joe is not stupid and Joe failed.
Geoff is the only teacher of Joe.
For all students and teachers, if the student is taught by the teacher and the student failed,
then either the student is stupid or there is is some other student with the same teacher who
also failed.
Therefore there is some student other than Joe, also taught by Geoff, who also failed.
Non-theorems
- Axioms
- Jon is the only human.
- Garfield, Arlene, and Nermal are the only (distinct) cats.
- Jon owns Garfield, but does not own Arlene.
- All cats love only one cat, and that cat is Garfield.
- Conjecture
- Jon owns all cats that love Garfield, except for Arlene.
- In TPTP format
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 ).
tff(only_jon,axiom, ! [H: human] : H = jon ).
tff(only_garfield_and_arlene_and_nermal,axiom,
! [C: cat] :
( C = garfield | C = arlene | C = nermal ) ).
tff(distinct_cats,axiom,
( garfield != arlene & arlene != nermal
& nermal != garfield ) ).
tff(jon_owns_garfield_not_arlene,axiom,
( owns(jon,garfield) & ~ owns(jon,arlene) ) ).
tff(all_cats_love_garfield,axiom,
! [C: cat] : ( loves(C) = garfield ) ).
tff(jon_owns_garfields_lovers,conjecture,
! [C: cat] :
( ( loves(C) = garfield & C != arlene )
=> owns(jon,C) ) ).
- Check the syntax using TPTP4X in
SystemB4TPTP.
- Check the axioms are satisfiable with Vampire-SAT in
SystemOnTPTP.
- Try prove it using Vampire in
SystemOnTPTP.
- Disprove it using Vampire-FMo
SystemOnTPTP.
That produces a (non-TPTP-compliant) finite countermodel.
Here's a counter model in the new TPTP format.
- View the finite countermodel using IIV in
SystemOnTSTP.
- Verify the finite countermodel using AGMV in
SystemOnTSTP.
Use the concatenation of the problem and the countermodel as input.