10
LOGICAL REASONING SYSTEMS
CÁC HỆ THỐNG LÝ LUẬN LOGIC (HỢP LÝ)
In which we show how to build efficient programs that reason with logic.
Trong phần này chúng tôi sẽ cho thấy làm thế nào để xây dựng được các chương trình hiệu quả, đó là lý luận hợp lý!
10.1 INTRODUCTION
10.1 GIỚI THIỆU
We have explained that it is a good idea to build agents as reasoning systems - systems that explicitly represent and reason with knowledge.
Chúng tôi đã giải thích rằng đó là một ý tưởng tốt để xây dựng các tác nhân theo hệ thống lý luận - hệ thống biểu diễn một cách rõ ràng và lý luận có kiến thức.
+
The main advantage of such systems is a high degree of modularity.
Ưu điểm chính của hệ thống như vậy là một mức độ cao của modul hóa.
+
The control structure can be isolated from the knowledge, and each piece of knowledge can be largely independent of the others.
Cấu trúc điều khiển có thể được phân lập từ kiến thức, và mỗi phần kiến thức có thể là phần lớn của những kiến thức độc lập khác.
10.4 THEOREM PROV
Theorem provers (also known as automated reasoners) differ from logic programming languages in two ways. First, most logic programming languages only handle Horn clauses, whereas theorem provers accept full first-order logic. Second, Prolog programs intertwine logic and control. The programmer's choice in writing A <= B A C instead of A •£= CA B affects the execution of the program. In theorem provers, the user can write either of these, or another form such as -*B •<= C A ->A, and the results will be exactly the same. Theorem provers still need control information to operate efficiently, but this information is kept distinct from the knowledge base,
rather than being part of the knowledge representation itself. Most of the research in theorem provers is in finding control strategies that are generally useful. In Section 9.6 we covered three generic strategies: unit preference, linear input resolution, and set of support.
Design of a theorem prover
In this section, we describe the theorem prover OTTER (Organized Techniques for Theorem-proving and Effective Research) (McCune, 1992), with particular attention to its control strategy.
In preparing a problem for OTTER, the user must divide the knowledge into four parts:
• A set of clauses known as the set of support (or sos), which defines the important facts about the problem. Every resolution step resolves a member of the set of support against another axiom, so the search is focused on the set of support.
• A set of usable axioms that are outside the set of support. These provide background
knowledge about the problem area. The boundary between what is part of the problem
(and thus in sos) and what is background (and thus in the usable axioms) is up to the user's judgment.
• A set of equations known as rewrites or demodulators. Although demodulators are
equations, they are always applied in the left to right direction. Thus, they define a
canonical form into which all terms will be simplified. For example, the demodulator
x + 0 = x say s that every term of the form x + 0 should be replaced by the term x.
• A set of parameters and clauses that defines the control strategy. In particular, the user specifies a heuristic function to control the search and a filtering function that eliminates some subgoals as uninteresting.
OTTER works by continually resolving an element of the set of support against one of the usable axioms. Unlike Prolog, it uses a form of best-first search. Its heuristic function measures the "weight" of each clause, where lighter clauses are preferred. The exact choice of heuristic is up to the user, but generally, the weight of a clause should be correlated with its size and/or difficulty.
Unit clauses are usually treated as very light, so that the search can be seen as a generalization of the unit preference strategy. At each step, OTTER moves the "lightest" clause in the set of support to the usable list, and adds to the usable list some immediate consequences of resolving the lightest clause with elements of the usable list. OTTER halts when it has found a refutation or when there are no more clauses in the set of support. The algorithm is shown in more detail in
Figure 10.5.
procedure OTTER(sos, usable)
inputs: sos, a set of support—clauses defining the problem (a global variable)
usable, background knowledge potentially relevant to the problem
repeat
clause <— the lightest member of sos
move clause from sos to usable
PROCESS(INFER(clause, usable), sos)
until sos - [ ] or a refutation has been found
____________________________________________________________________________________
function INFER(clause, usable) returns clauses
resolve clause with each member of usable
return the resulting clauses after applying FILTER
____________________________________________________________________________________
procedure PROCESS(clauses, sos)
for each clause in clauses do
clause <- SlMPLIFY(clauses)
merge identical literals
discard clause if it is a tautology
sos <— [clause I sos]
if clause has no literals then a refutation has been found
if clause has one literal then look for unit refutation
end
Figure 10.5 Sketch of the OTTER theorem prover. Heuristic control is applied in the selection of the "lightest" clause, and in the FILTER function that eliminates uninteresting clauses from consideration.
Extending Prolog
An alternative way to build a theorem prover is to start with a Prolog compiler and extend it to get a sound and complete reasoner for full first-order logic. This was the approach taken in the Prolog Technology Theorem Prover, or PTTP (Stickel, 1988). PTTP includes five significant changes to Prolog to restore completeness and expressiveness:
• The occurs check is put back into the unification routine to make it sound.
• The depth-first search is replaced by an iterative deepening search. This makes the search strategy complete and takes only a constant factor more time.
• Negated literals (such as ~^P(x)) are allowed. In the implementation, there are two separate routines, one trying to prove P and one trying to prove -iP.
• A clause with n atoms is stored as n different rules. For example, A -4= B A C would also be stored as -A and as ->C <= B A ->A. This technique, known as locking, means that the current goal need only be unified with the head of each clause but still allows for proper handling of negation.
• Inference is made complete (even for non-Horn clauses) by the addition of the linear input resolution rule: If the current goal unifies with the negation of one of the goals on the stack, then the goal can be considered solved. This is a way of reasoning by contradiction. Suppose we are trying to prove P and that the current goal is ->P. This is equivalent to saying that ->P => P, which entails P
Despite these changes, PTTP retains the features that make Prolog fast. Unifications are still done by modifying variables directly, with unbinding done by unwinding the trail during backtracking. The search strategy is still based on input resolution, meaning that every resolution is against one of the clauses given in the original statement of the problem (rather than a derived clause). This makes it feasible to compile all the clauses in the original statement of the problem.
The main drawback of PTTP is that the user has to relinquish all control over the search for solutions. Each inference rule is used by the system both in its original form and in the contrapositive form. This can lead to unintuitive searches. For example, suppose we had the rule
(f(x, y) =f(a, b)) ^.(X = d)/\(y = b)
As a Prolog rule, this is a reasonable way to prove that two/ terms are equal. But PTTP would also generate the contrapositive:
(x#a) <= (f(x,y)#f(a,b)) A (y = b)
It seems that this is a wasteful way to prove that any two terms x and a are different.
Theorem provers as assistants
So far, we have thought of a reasoning system as an independent agent that has to make decisions and act on its own. Another use of theorem provers is as an assistant, providing advice to, say, a mathematician. In this mode the mathematician acts as a supervisor, mapping out the strategy for determining what to do next and asking the theorem prover to fill in the details. This alleviates the problem of semi-decidability to some extent, because the supervisor can cancel a query and try another approach if the query is taking too much time. A theorem prover can also act as a proof-checker, where the proof is given by a human as a series of fairly large steps; the individual inferences required to show that each step is sound are filled in by the system.
A Socratic reasoner is a theorem prover whose ASK function is incomplete, but which can always arrive at a solution if asked the right series of questions. Thus, Socratic reasoners make good assistants, provided there is a supervisor to make the right series of calls to ASK. ONTIC (McAllester, 1989) is an example of a Socratic reasoning system for mathematics. of an agent—on each cycle, we add the percepts to the knowledge base and run the forward chainer, which chooses an action to perform according to a set of condition-action rules.
Theoretically, we could implement a production system with a theorem prover, using
resolution to do forward chaining over a full first-order knowledge base. A more restricted language, on the other hand, can provide greater efficiency because the branching factor is reduced. The typical production system has these features:
• The system maintains a knowledge base called the working memory. This contains a set of positive literals with no variables.
• The system also maintains a separate rule memory. This contains a set of inference rules, each of the form p\ A pi • • • =>• act\ A act^ • • •, where the /?, are literals, and the act, are actions to take when the pi are all satisfied. Allowable actions are adding and deleting elements from the working memory, and possibly other actions (such as printing a value).
• In each cycle, the system computes the subset of rules whose left-hand side is satisfied by the current contents of the working memory. This is called the match phase.
• The system then decides which of the rules should be executed. This is called the conflict resolution phase.
• The final step in each cycle is to execute the action(s) in the chosen rule(s). This is called the act phase.
Match phase
Unification addresses the problem of matching a pair of literals, where either literal can contain variables. We can use unification in a straightforward way to implement a forward-chaining production system, but this is very inefficient. If there are w elements in working memory and r rules each with n elements in the left-hand side, and solving a problem requires c cycles, then the naive match algorithm must perform wrnc unifications. A simple expert system might have w= 100, r = 200, n = 5, c = 1000, so this is a hundred million unifications. The rete algorithm4 used in the OPS-5 production system was the first to seriously address this problem. The rete algorithm is best explained by example. Suppose we have the following rule memory:
and the following working memory:
{A(1),A(2),B(2),B(3),B(4),C(5)}
The rete algorithm first compiles the rule memory into the network shown in Figure 10.6. In this diagram, the circular nodes represent fetches (not unifications) to working memory. Under node A, the working memory elements A(l) and A(2) are fetched and stored. The square nodes indicate unifications. Of the six possible A x B combinations at the A = B node, only A(2) and B(2) satisfy the unification. Finally, rectangular boxes indicate actions. With the initial working
4
Rete is Latin for net. It rhymes with treaty.
Figure 10.6 A rete network. Circles represent predicate tests. A square containing, for
example, A=B represents a constraint that the solutions to the A and B tests must be equal.
Rectangles are actions.
memory the "add D" rule is the only one that fires, resulting in the addition of the sentence D(2) to working memory.
One obvious advantage of the rete network is that it eliminates duplication between rules. All three of the rules start with a conjunction of A and B, and the network allows that part to be shared. The second advantage of rete networks is in eliminating duplication over time. Most production systems make only a few changes to the knowledge base on each cycle. This means that most of the tests at cycle t+\ will give the same result as at cycle t. The rete network modifies itself after each addition or deletion, but if there are few changes, then the cost of each update will be small relative to the whole job of maintaining the indexing information. The network
thus represents the saved intermediate state in the process of testing for satisfaction of a set of conjuncts. In this case, adding D(2) will result in the activation of the "add E" rule, but will not have any effect on the rest of the network. Adding or deleting an A, however, will have a bigger effect that needs to be propagated through much of the network.
Conflict resolution phase
Some production systems execute the actions of all rules that pass the match phase. Other production systems treat these rules only as suggestions, and use the conflict resolution phase to decide which of the suggestions to accept. This phase can be thought of as the control strategy. Some of the strategies that have been used are as follows:
• No duplication. Do not execute the same rule on the same arguments twice.
• Recency. Prefer rules that refer to recently created working memory elements.
• Specificity. Prefer rules that are more specific.
5
For example, the second of these two rules
would be preferred:
Mammal(x) => add Legs(x, 4)
Mammal(x) A Human(x) =>• add Legs(x, 2)
• Operation priority. Prefer actions with higher priority, as specified by some ranking. For example, the second of the following two rules should probably have a higher priority:
ControlPanel(p) A Dusty(p) => Action(Dust(p))
ControlPanel(p) A MeltdownLightOn(p) => Action(Evacuate)
Practical uses of production systems
Forward-chaining production systems formed the foundation of much early work in AI. In par-ticular, the XCON system (originally called Rl (McDermott, 1982)) was built using a production system (rule-based) architecture. XCON contains several thousand rules for designing configura-tions of computer components for customers of the Digital Equipment Corporation. It was one of the first clear commercial successes in the emerging field of expert systems. Many other similar systems have been built using the same underlying technology, which has been implemented
in the general-purpose language Ops-5. A good deal of work has gone into designing match-ing algorithms for production system languages, as we have seen; implementations on parallel hardware have also been attempted (Acharya et al., 1992).
ARCHITECTURES Production systems are also popular in cognitive architectures—that is, models of human reasoning—such as ACT (Anderson, 1983) and SOAR (Laird et al., 1987). In such systems, the "working memory" of the system models human short-term memory, and the productions are part of long-term memory. Both ACT and SOAR have sophisticated mechanisms for conflict resolution, and for saving the results of expensive reasoning in the form of new productions. These can be used to avoid reasoning in future situations (see also Section 21.2).
