First-order Logic (FOF)
New logic features
- Predicates with arguments are true or false (boolean)
- Constants and functions with arguments (things in the world)
- Universally quantified variables (for all)
- Existentially quantified variables (there exists)
- Equality as a primitive
Problem
- Axioms
- The USA is a country.
- The capital of every country is a beautiful big city
- There is some city that is the capital of the USA
- Every big city has crime.
- A big city is a city.
- Conjecture
- Therefore, there is some city that is beautiful but has crime.
In logic
- Quantifiers: ∀ ∃
- Equality: = ≠
- Axioms
- country(usa)
- ∀ C (country(C) → (big_city(capital_of(C)) ∧ beautiful(capital_of(C)) ))
- ∃ C (city(C) ∧ C = capital_of(usa))
- ∀ C (big_city(C) → has_crime(C))
- ∀ C (big_city(C) → city(C))
- Conjecture
- ∃ C (city(C) ∧ beautiful(C) ∧ has_crime(C))
In TPTP format
- Predicates, constants, functions: start lowercase, contain alphanumerics and underscore.
- Quantifiers: ! ?
- Infix equality = !=
- Unique Names $distinct, e.g.,$distinct(usa,brazil,australia,japan).
Not a closed world assumption.
- fof annotated formulae have a name (lowercase), a role (axiom,
conjecture, and others), a formula, and end with .
-
fof(usa,axiom, country(usa) ).
fof(country_big_city,axiom,
! [C] : ( country(C) => ( big_city(capital_of(C)) & beautiful(capital_of(C)) ) ) ).
fof(usa_capital_axiom,axiom,
? [C] : ( city(C) & C = capital_of(usa) ) ).
fof(crime_axiom,axiom,
! [C] : ( big_city(C) => has_crime(C) ) ).
fof(big_city_city,axiom,
! [C] : ( big_city(C) => city(C) ) ).
fof(some_beautiful_crime,conjecture,
? [C] : ( city(C) & beautiful(C) & has_crime(C) ) ).
- 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
Bob, Maggie, Jill, and Geoff are four distinct people.
The oldest sibling of Geoff is Jill (hint - a person has only one oldest sibling).
If any person's oldest sibling is good looking then that person is good looking.
If any person is good looking then one (or both) of their parents is good looking
(hint - think of parent-child as a relationship between two people).
Jill is good looking, Bob is not.
The (only) parents of Geoff are Bob and Maggie.
Therefore, Maggie is good looking.
Non-theorems
- Axioms
- Iokaste, Oedipus, Polyneikes, and Thersandros are different people
- Iokaste is a parent of Oedipus and Polyneikes
- Oedipus is a parent of Polyneikes
- Polyneikes is a parent of Thersandros
- Nobody is their own parent
- Oedipus is a patricide
- Thersandros is not a patricide
- Conjecture
- Iokaste is a parent of a patricide who is a parent of somebody who is not a patricide
- In TPTP format
fof(different_people,axiom,
( iokaste != oedipus & iokaste != polyneikes & iokaste != thersandros
& oedipus != polyneikes & oedipus != thersandros
& polyneikes != thersandros ) ).
fof(iokaste_oedipus,axiom,
( parent_of(iokaste,oedipus) & parent_of(iokaste,polyneikes) ) ).
fof(oedipus_polyneikes,axiom,
parent_of(oedipus,polyneikes) ).
fof(polyneikes_thersandros,axiom,
parent_of(polyneikes,thersandros) ).
fof(no_self_parent,axiom,
! [X] : ~ parent_of(X,X) ).
fof(oedipus_patricidal,axiom,
patricide(oedipus) ).
fof(thersandros_not_patricidal,axiom,
~ patricide(thersandros) ).
fof(iokaste_parent_particide_parent_not_patricide,conjecture,
? [P,NP] :
( parent_of(iokaste,P) & patricide(P) & parent_of(P,NP)
& ~ patricide(NP) ) ).
- Check the syntax using TPTP4X in
SystemB4TPTP.
- Check the axioms are consistent with Vampire-SAT in
SystemOnTPTP.
- Try prove it using Vampire in
SystemOnTPTP.
- Change the conjecture to "Iokaste is a parent of a patricide who is a parent of
somebody who is a patricide"
- Try prove it using Vampire in
SystemOnTPTP.
That produces a saturation as a countermodel.
- Disprove it using Paradox
SystemOnTPTP.
That produces a finite countermodel.
- 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.