Skip to Main Content
Automated Planning
book

Automated Planning

by Malik Ghallab, Dana Nau, Paolo Traverso
May 2004
Intermediate to advanced content levelIntermediate to advanced
635 pages
19h 46m
English
Morgan Kaufmann
Content preview from Automated Planning
B.3 First-Order Logic 557
2. A is false, and therefore C
2
is true and can be eliminated, while A can be
eliminated from C
1
.
In the limiting case, in which C
1
and C
2
are unit clauses and the two literals are
complementary, the resolution principle generates the empty clause .
If C is a resolvent of C
1
and C
2
, we say that C logically follows from C
1
and
C
2
. We can now define the notion of deduction based on resolution. Given a set
of clauses S,adeduction of the clause C from S is a finite sequence C
1
, ..., C
n
of clauses such that each C
i
either is a clause in S or is a resolvent of clauses
preceeding C
i
, and C
n
= C. A deduction of the empty clause from S is called
a refutation of S.
Example B.3 Let us build a deduction of p r from p q and q r, i.e.,
Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month,
and much more.
Start your free trial

You might also like

Communicate with Teams More Effectively

Communicate with Teams More Effectively

Charles Humble
How to Overcome a Power Deficit

How to Overcome a Power Deficit

Cyril Bouquet, Jean-Louis Barsoux

Publisher Resources

ISBN: 9781558608566