Predicate (1st order) Logic
It is relatively easy to check for logical consequence in proposition logic because propositional
logic is not very expressive.
It is desirable to have a more expressive logic in which to write the axioms and conclusions.
A primary weakness of propositional logic is the lack of syntax for representing objects in the
domain of interest; propositional logic only permits statements about the domain of interest,
e.g., it is not possible to have a symbol for Socrates, rather it is possible only to
make statements about Socrates.
Associated with this is the absence of functional abstraction, e.g., it is not possible to refer
to the brother of Socrates.
A second weakness of propositional logic is that it does not provide variables which can be
quantified over, e.g., it is not possible to represent the all men in
All men are mortal by a variable which can range of the possible values of specific men.
Similarly, it is not possible to claim the existence of something with a given property by
representing that something by a variable, as in "There exists a prime number greater than 27".
1st order logic overcomes these weaknesses of propositional logic by providing a richer language.
The cost of this increased expressivity is the loss of decidability for logical consequence.
1st order logic is semi-decidable, which means that if a formula is a logical consequence of a
set of axioms, it is possible to show that it is.
However, if a formula is not a logical consequence of a set of axioms, it may not be possible to
show that it is not.
In addition, 1st order logic requires more complex mechanisms for checking for logical consequence.
The Language of 1st order logic
A 1st order language consists of three 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.
Prolog syntax is used here: variables start with upper case alphbetic, and functors and predicate
symbols start with lower case alphabetic.
Functors and predicate symbols are distinguished by the context, as described below.
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 = { geoff/0, jim/0, brother_of/1 }
P = { wise/1, taller/2 }
|
From the components of the language, two types of expressions are built.
This is in contrast to propositional logic where only propositions exist.
The first type of expression is terms.
Terms are used to denote (possibly arbitrary) objects in the domain of interest.
Terms thus correspond roughly to data in conventional programming.
Terms are defined recursively by:
- A functor of arity 0 (a constant) is a term
- A variable is a term
- A functor with the appropriate number of terms as arguments, is a term.
Example
|
---|
geoff
Person
brother_of(jim)
brother_of(brother_of(X))
|
Note that if there is a functor of arity greater than 0, then there is an infinite number of terms.
As might be expected, ATP for 1st order logic is much easier if the number of terms is finite
(in fact it reduces to ATP for propositional logic).
For this reason, it is desirable to formulate ATP problems without any functors of arity greater
than 0.
The second type of expression is atoms, which correspond to the propositions of
propositional logic.
Atoms decribe relationships between terms (objects in the domain).
Atoms are defined by:
- A predicate symbol of arity 0 (a proposition) is an atom
- A predicate symbol with the appropriate number of terms as arguments, is an atom.
Example
|
---|
wise(geoff)
taller(Person,brother_of(jim))
wise(brother_of(brother_of(X)))
|
If the number of terms is infinite (which occurs if there is a functor of arity greater than 0),
and there is a predicate symbol of arity greater than 0, then there is an infinite number of atoms.
Connectives are used to combine atoms into the formulae of 1st order logic.
The connectives include all those used in propositional logic, and two new quantifiers:
- ~ for negation.
- ∧ or & for conjunction.
- ∨ or | for disjunction.
- => for implication.
- <=> for equivalence.
- <~> for exclusive or.
- ∀ or ! for universal quantification.
This corresponds to saying "for all" in English, e.g.,
∀X (man(X) => mortal(X))
says "for all objects X, X is a man implies X is mortal".
It is easy to remember that ∀ means "for all" by noticing that the
∀ is an upside down A from for All.
- ∃ or ? for existential quantification.
This corresponds to saying "there exists" in English, e.g.,
∃X (prime(X) & greater(X,27))
says "There exists an object X such that X is a prime number and X is greater than 27".
It is easy to remember that ∃ means "there exists" by noticing that the
∃ is a backwards E from there Exists.
Denoting arbitary 1st order formulae by uppercase variable letters,
e.g., P, 1st order formulae are defined recursively by:
- Atoms are formulae
- If P and Q are formulae then
~P,
P & Q,
P | Q,
P => Q,
P <=> Q, and
(P) are formulae.
- If P is a formula and X is a variable, then
∀X P and
∃X P are formulae.
The ∀X and
∃X are called
quantifications of X, and they quantify all occurrences of X in
P.
The quantification has precedence over any earlier (to the left) quantification of X.
Variables with the same name but which are quantified by different quantifiers, are different
variables.
The precedence order of the above operators is ∀ ∃ ~ & | => <=>, i.e.,
∀ and ∃ bind most tightly, down to <=>.
This precedence ordering allows some brackets to be omitted, e.g.,
∀X (clever(X) => pass(X) | lazy(X))
means
∀X (clever(X) => (pass(X) | lazy(X))).
Note that the ()s round the (clever(X) => pass(X) | lazy(X)) are necessary, for
otherwise the quantification would apply to only the clever(X).
Example
|
---|
wise(geoff)
~taller(Person,brother_of(jim))
wise(geoff) & wise(brother_of(brother_of(Person)))
~taller(Person,brother_of(jim)) | wise(brother_of(brother_of(Person)))
wise(brother_of(brother_of(Person)) => wise(geoff)
wise(geoff) <=> ~taller(Person,brother_of(jim))
(wise(geoff) & wise(brother_of(brother_of(Person)))) | wise(geoff)
∀Person ~taller(Person,brother_of(jim))
∃Person wise(brother_of(brother_of(Person)) => wise(geoff)
|
Atoms and the negations of atoms are called literals.
Example
|
---|
wise(brother_of(X))
~taller(geoff,jim)
|
Ground formulae are formulae that contain no variables.
Example
|
---|
wise(geoff)
wise(geoff) <=> ~taller(geoff,brother_of(jim))
|
The scope of a quantification is the formula which follows the quantification, e.g.,
the scope of ∃Person in
∃Person wise(brother_of(brother_of(Person)) =>
wise(geoff)
is
wise(brother_of(brother_of(Person)).
A variable is bound if it occurs in a quantification or it is within the scope of a
quantification of that variable.
Otherwise a variable is free.
A formulae that has no free variables is a closed formula; otherwise a formula is
open.
Example
|
---|
Person is bound in in the closed formula:
∀Person ~taller(Person,brother_of(jim))
Person is free in the open formula:
~taller(Person,brother_of(jim))
Person is bound and free in the open formula:
∀Person ~taller(Person,jim) | wise(Person)
Person is bound in the closed formula:
∀Person(~taller(Person,jim) | wise(Person))
|
A free variable in a expression can be instantiated with a term, thus binding
the variable to that value and forming an instance of the expression.
Example
|
---|
The free variable Person in:
~taller(Person,brother_of(jim))
can be instantiated with brother_of(geoff) to form the instance:
~taller(brother_of(geoff),brother_of(jim))
|
For ATP open formulae are not useful, because it is not possible to interpret (in the sense of
giving meaning) open formulae.
Open formulae can be closed by universal or existential quantification.
This is done by placing either a universal or existential quantifier in front of the bracketed
formula.
The free standing quantifier notation is shorthand for a universal or existential quantification
of every free variable in the formula.
Example
|
---|
~taller(Person,brother_of(jim)) | wise(brother_of(brother_of(Person)))
can be closed either universally:
∀(~taller(Person,brother_of(jim)) | wise(brother_of(brother_of(Person))))
or existentially:
∃(~taller(Person,brother_of(jim)) | wise(brother_of(brother_of(Person))))
|
In English universal quantification is usually meant if no explicit quantification is given,
e.g., "Sheep are stupid" usually means "All sheep are stupid", not "There exists a sheep that
is stupid".
Equality
Many domains require the use of the notion of equality.
In 1st order logic equality statements use the equal/2 predicate, or infix
=/2 and !=/2 predicates.
Example
|
---|
even(sum(two_squared,b))
two_squared = four
∀X
(zero(X) => difference(four,X) = sum(four,X))
zero(b)
even(difference(two_squared,b))
|
Although the conjecture may seem like a logical consequence to humans, that's because humans
"know" what equal means (even without knowing what the "math" means).
In reality, many modern ATP systems do "know" what equal means, and for such systems
it is not necessary to
add in the axioms of equality.
Translation from English to 1st Order Logic
There is often a direct translation from a problem stated in a natural language to 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
- Translate the axioms.
- Make appropriate definitions for the predicates and functors.
- Translate the conjecture.
Example
|
---|
There is a barbers' club that obeys the following three conditions:
- The (only) four of the members are Guido, Lorenzo, Petrucio, and Guido's nephew.
- If any member A has shaved any other member B - whether himself or another - then all
members have shaved A.
- Guido has shaved his nephew.
Prove Petrucio has shaved Lorenzo
|
V = { V : V starts with uppercase }
F = { guido/0, lorenzo/0, petrucio/0, nephew_of/1 }
P = { member/1, shaved/2, all_shaved/1 }
|
- The (only) four of the members are Guido, Lorenzo, Petrucio, and
Guido's nephew.
member(guido)
member(lorenzo)
member(petrucio)
member(nephew_of(guido))
∀M (member(M) => (M = guido | M = lorenzo | M = petrucio | M = nephew_of(guido)))
- If any member A has shaved any other member B - whether himself or another - then all
members have shaved A.
∀M1∀M2
( (member(M1) & member(M2) & shaved(M1,M2)) => all_shaved(M1) )
- Guido has shaved his nephew.
shaved(guido,nephew_of(guido))
- Definitions
∀M1 (
all_shaved(M1) <=> ( member(M1) &
∀M2
(member(M2) => shaved(M2,M1)) ) )
- Petrucio has shaved Lorenzo.
shaved(petrucio,lorenzo)
|
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.
|
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 }
|
- Every student is enrolled in at least one course.
! [S] : ( student(S) => ? [C] : ( course(C) & enrolled(S,C) ) )
- Every professor teaches at least one course.
! [P] : ( professor(P) => ? [C] : ( course(C) & teaches(P,C) ) )
- Every course has at least one student enrolled.
! [C] : ( course(C) => ? [S] : ( student(S) & enrolled(S,C) ) )
- Every course has at least one professor teaching it.
! [C] : ( course(C) => ? [P] : ( professor(P) & teaches(P,C) ) )
- The coodinator of a course is a professor who is teaching it.
! [C] :
( course(C)
=> ( 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,C] :
( ( student(S) & course(C) & enrolled(S,C) )
=> ! [P] :
( ( professor(P) & teaches(P,C) )
=> taught_by(S,P) ) )
- CSC410 is a course.
course(csc410)
- Michael is a student enrolled in CSC410.
( student(michael) & enrolled(michael,csc410) )
- Victor is the coordinator of CSC410.
coordinator_of(csc410) = victor
- Victor teaches Michael.
taught_by(michael,victor)
|
Educational Example
For many more ideas and suggestions, see Peter Stuber's
Translation Tips.
Exercises
Convert the following into 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.
- Garfield is a cat.
Odie is a dog.
Cats and dogs are animals.
Jon is a human.
Every animal has a human owner.
Jon is the owner of Garfield and Odie.
Garfield and Odie are the only animals that Jon owns.
If a cat is chased by a dog, then the owner of the cat hates the owner of the dog.
Odie has chased Garfield.
Therefore, Jon hates himself.
- 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.
The basic notion of set theory is membership of a set.
Using a member/2 predicate, define set equality, intersection, union, power set,
empty set, and diifference.
For example, intersection is defined as:
! [X,A,B] :
( member(X,intersection(A,B))
<=> ( member(X,A)
& member(X,B) ) )
Now write conjectures for transitivity of subset, associativity of set intersection, and
distribution of intersection over union.
Equality Axioms
Example
|
---|
even(sum(two_squared,b))
two_squared = four
∀X
(zero(X) => difference(four,X) = sum(four,X))
zero(b)
even(difference(two_squared,b))
|
Although the conjecture may seem like a logical consequence to humans, that's because humans
"know" what equal means (even without knowing what the "math" means).
However, there are many models of the axioms that are not a models of
the conjecture, e.g., simply by making even(sum(four,b))
be FALSE.
Such models are possible because the axioms are missing definitions
for equality.
These definitions are the axioms of equality, and must be included to
force equality to have its usual meaning.
They are:
- Reflexivity - everything equals itself
- Symmetry - If X equals Y then
Y equals X
- Transitivity - If X equals Y and
Y equals Z, then
X equals Z
∀X (X = X)
∀X
∀Y
(X = Y => Y = X)
∀X
∀Y
∀Z
((X = Y & Y = Z) => X = Z)
- Function substitution - If X equals Y
then f(X) equals f(Y).
For every argument position of every functor.
- Predicate substitution - If X equals Y and
p(X) is TRUE, then p(Y)
is TRUE
For every argument position of every predicate.
∀X
∀Y
∀Z
(X = Y => sum(X,Z) = sum(Y,Z))
∀X
∀Y
∀Z
(X = Y => sum(Z,X) = sum(Z,Y))
∀X
∀Y
∀Z
(X = Y => difference(X,Z) = difference(Y,Z))
∀X
∀Y
∀Z
(X = Y => difference(Z,X) = difference(Z,Y))
∀X
∀Y
((X = Y & even(X)) => even(Y))
∀X
∀Y
((X = Y & zero(X)) => zero(Y))
In reality, many modern ATP systems do "know" what equal means,
and for such systems it is not necessary to add in the axioms of equality.
Exercises
Convert the following into 1st order logic, and generate the required
axioms of equality:
Someone who lives in Dreadbury Mansion killed Aunt Agatha.
Agatha, the butler, and Charles live in Dreadbury Mansion,
and are the only people who live therein. A killer always
hates his victim, and is never richer than his victim.
Charles hates no one that Aunt Agatha hates. Agatha hates
everyone except the butler. The butler hates everyone not
richer than Aunt Agatha. The butler hates everyone Aunt
Agatha hates. No one hates everyone. Agatha is not the
butler. Therefore : Agatha killed herself.
Interpretation
Interpretation of 1st order formulae requires a more complex structure
than for propositional logic, because there are "component parts" of
1st order formulae.
If the Herbrand base is finite (due to a finite Herbrand universe) then
it is possible to assign truth values to elements of the Herbrand base.
In this case logical consequence can be decided as for propositional
logic, using a truth table.
Otherwise, as is the case when the full expressive power of 1st order
logic is used, a more complex structure is required.
Henceforth only the latter, more complex, 1st order languages are
considered.
An interpretation of a 1st order logic consists of three parts:
- D is the domain of the interpretation.
- F provides a function for each function symbol, from domain elements
to the domain.
- P provides a function for each predicate symbol, from domain elements
to the truth values TRUE and FALSE.
Example
|
---|
One possible interpretation of the language
V = { V : V starts with uppercase }
F = { geoff/0, jim/0, brother_of/1 }
P = { wise/1, taller/2 }
is
D = { , }
F = { geoff → ,
jim → ,
brother_of( ) → ,
brother_of( ) → }
P = { wise( ) → TRUE,
wise( ) → TRUE,
taller( , ) → FALSE,
taller( , ) → FALSE,
taller( , ) → TRUE,
taller( , ) → FALSE }
|
As with propositional logic, all the possible Rs can be presented as a truth table or
a semantic tree.
Given an interpretation, the truth value of a closed formula can be determined, with respect
to that interpretation.
The procedure for ground formula is:
- Map all constants to the domain.
- Repeatedly map functions of domain elements to domain elements, until only predicates of
domain elements remain.
- Map the predicates of domain elements to truth values.
- Combine the truth values according to the truth tables for the connectives.
Note that as this procedure is for ground formulae, quantifiers do not need to be
interpreted here.
Non-ground closed formulae are interpreted as follows:
- A universally quantified formula is TRUE iff
the unquantified formula is TRUE with the quantified
variable instantiated to each of the domain elements.
- An existentially quantified formula is TRUE iff
the unquantified formula is TRUE with the quantified
variable instantiated to at least one of the domain elements.
Example
|
---|
To interpret the universally quantified formula
∀Person (~taller(Person,jim) | wise(Person)),
the universally quantified variable Person is
instantiated to all the domain elements.
- Person =
~taller( ,jim) | wise( )
~taller( , ) | wise( )
~FALSE | TRUE
TRUE | TRUE
TRUE
- Person =
~taller( ,jim) | wise( )
~taller( , ) | wise( )
~FALSE | TRUE
TRUE | TRUE
TRUE
The unquantified formula is TRUE with the quantified
variable instantiated to each of the domain elements, thus the
universally quantified formula is TRUE.
|
Example
|
---|
To interpret the existentially quantified formula
∃Person ( wise(brother_of(brother_of(Person))) => wise(geoff))
the existentially quantified variable Person is
instantiated to find a TRUE instance of the formula.
The unquantified formula is TRUE with the quantified
variable instantiated to at least one of the domain elements, thus the
existentially quantified formula is TRUE.
|
If the domain of the interpretation is finite, interpretation of closed
1st order formulae is a finite process.
If the domain is inifinite it is not possible to determine that a
universally quantified formula is TRUE, nor is it possible
to determine that an existentially quantified formula is FALSE.
Some Interpretations
In general, an interpretation must have the structure discussed above.
However, interpreting a formula in such a general structure can be very
expensive.
There are some simple interpretations in which the interpretation of a
literal can be determined syntactically.
- The positive interpretation maps all atoms to TRUE.
- The negative interpretation maps all atoms to FALSE.
- A predicate partition, which divides the predicate symbols of the
1st order language into two partitions P1 and P2,
map atoms whose predicate symbols are in P1 to
TRUE and atoms whose predicate symbols are in
P2 to FALSE.
The Quest for Logical Consequence
To show that C is a logical consequence of Ax, it is necessary to:
- Show that every model of Ax is a model of C
OR
- Show that S' = Ax ∪ {~C} is unsatisfiable.
For every 1st order language there is an infinite number of possible
interpretations.
New interpretations can be constructed by changing the domain and by
changing the F and R mappings.
Thus it is not possible to use the "table" method from propositional
logic, as there is an infinite number of rows to check.
- Show that S' is unsatisfiable.
Satisfiability Preserving Transformations
One of the techniques for establishing that C is a logical
consequence of Ax is to show that Ax ∪ {~C}
is unsatisfiable.
Thus the ability to detect that a set of formulae is unsatisfiable, is
important.
It may be difficult or impossible to show directly that a set is
unsatisfiable.
A satisfiability preserving transformation (SPT) takes a set of
formulae and transforms it to a new set, such that if the original set is
satisfiable then so is the transformed set.
Conversely, if the transformed set is unsatisfiable then so is the
original set.
If, by repetitive use, the application of SPTs produces a set that is
obviously unsatisfiable (e.g., containing FALSE) from a set of
formulae, then, iteratively, this means that the very original set is
also unsatisfiable.
If the original set is of the form Ax ∪ {~C}, this establishes
that C is a logical consequence of Ax.
The process of producing a set that is obviously unsatisfiable is called
finding a refutation.
Logical Inference
An inference rule infers formulae from parent formulae.
An inference rule is sound if it infers only logical consequences
of its parents.
The operation of applying a sound inference rule to parents from a set, and
then adding the inferred formula back into the set, is a SPT (think why!).
(There are other SPTs, but this is an important one.)
Thus sound inference rules form the basis of a a simple algorithm for
establishing logical consequence.
The basic saturation procedure is :
Form the set Ax ∪ {~C}
While a refutation has not been found
Copy formulae from the set
Generate logical consequences
Put logical consequences into the set
Note the "Copy", indicating that a formula may be used multiple
times with a new set of variables each time.
An inference system is complete if, by repetitive use, it can infer
every logical consequence of its input.
An inference system is refutation complete if, by repetitive use, it
can infer FALSE (a contradiction) from every unsatisfiable set.
Note: A complete inference system can infer all logical consequences, while a
refutation complete inference system can only check (via the unsatisfiability
idea) for logical consequence.
Exam Style Questions
- What are the two major limitations of propositional logic?
- What are the three components of a 1st order logic language?
- Which or the following formulae are {ground, closed}?
<insert some formulae here>
- What is important about closed formulae?
- Translate the following into 1st order logic:
Suming, Yi, and Yury are students, and are the only three students.
If a student works hard then they get a good grade.
At least one of the students works hard.
Therefore at least one student will get a good grade.
- Express the following scenario and conclusion in 1st order logic, in
a form ready to be converted to clause normal form.
There are some students who fail.
If a student fails, then either there is a lecturer who has taught the
student badly, or the student is stupid.
No lecturer teaches any student badly.
Therefore there is some student who is stupid.
- In what circumstances is it necessary to add the axioms of equality to
the formulae of a problem?
- Name the five (groups of) axioms of equality.
- What axioms of equality are needed with this formula?
p(X) | ~p(f(cat,dog)) | equal(X,cat)
- What are the three components of an interpretation of a first order
language? Give an example for the language:
V = { V : V starts with uppercase }
F = { coke/0, pepsi/0, competitor/1 }
P = { fizzy/1, sells-more/2 }
- Given the 1 st order logic language:
V = { V : V starts with uppercase }
F = { holden/0, ford/0, honda/0 main_competitor/1 }
P = { fast/1, faster/2 }
and the interpretation:
D = { commodore, laser, prelude }
F = { holden → commodore,
ford → laser,
honda → prelude,
main_competitor(commodore) → prelude,
main_competitor(laser) → prelude,
main_competitor(prelude) → commodore }
P = { fast(commodore) → TRUE,
fast(laser) → FALSE,
fast(prelude) → TRUE,
faster(commodore,commodore) → FALSE,
faster(commodore,laser) → TRUE,
faster(commodore,prelude) → TRUE,
faster(laser,commodore) → FALSE,
faster(laser,laser) → FALSE,
faster(laser,prelude) → FALSE,
faster(prelude,commodore) → FALSE,
faster(prelude,laser) → TRUE,
faster(prelude,prelude) → FALSE }
Show the steps of the interpretation of:
- faster(main_competitor(laser),commodore)
- fast(main_competitor(main_competitor(prelude))
- forall X ( faster(main_competitor(X),laser) & fast(X) )
- exists X ( fast(main_competitor(main_competitor(X))) |
forall Y faster(X,Y) ) )
- What are the positive and negative interpretations?
- Explain why truth tables cannot be used to establish logical consequence in lst order logic.
- What does it mean for an inference system to be {sound, complete, refutation complete}?
Which of these properties are desireable in an CNF based ATP system?
- Explain how unsatisfiability can be used to establish logical consequence in classical logic.