NASA Contractor Report 181827 

FORMAL VERIFICATION OF 

AI SOFTWARE 

(NASA-CR-181827) PORaAL VERIPICATIO# - OF AI 

SOFTYARB Final Report (sa1 International 

Corp.) 156 p CSCL 098 

N 8 9- 24 8 1 1 

Unclas 

G3/61 0217233 

John Rushby, R. Alan Whitehurst 

SRI International 

Computer Science Laboratory 

333 Ravenswood Avenue 

Menlo Park, CA 94025 

NASA Contract 18226 (Task 5) 

February 1989 

National Aeronautics and 

Space Administration 

Langley Research Center 

Hampton, Virginia 23665-5225 
, 

Abstract 

The application of formal verification techniques to AI software, particularly 

expert systems, is investigated. Constraint satisfaction and model inversion 

are identified as two formal specification paradigms for different classes of 

expert systems. A formal definition of consistency is developed, and the 

notion of approximate semantics is introduced. Examples are given of how 

these ideas can be applied in both declarative and imperative forms. 
Contents 

1 Introduction 1 

1.1 Formal Verification ........................ 2 

1.2 AI Software and Expert Systems ................ 4 

2 Requirements and Speciilcations 7 

2.1 Safety and Liveness Properties ................. 8 

2.2 Classification of Expert System Applications ......... 9 

2.2.1 Constraint Satisfaction Problems ............ 10 

2.2.2 Model Inversion Problems ................ 10 

2.2.2.1 Abduction ................... 13 

2.3 Formal Requirements Specifications ............... 13 

3 Languages 15 

3.1 Declarative Semantics ...................... 15 

3.2 Operational Semantics ...................... 16 

3.3 Approximate Semantics ..................... 19 

3.3.1 Approximate Declarative Semantics .......... 19 

3.3.2 Approximate Imperative Semantics ........... 24 

4 Examples 27 

4.1 Introduction ............................ 27 

4.2 Example-Constraint Satisfaction ................ 27 

4.2.1 Problem Description ................... 28 

4.2.2 Rule-Based Implementation ............... 28 

4.2.3 Requirements ....................... 30 

4.2.4 Formal Specification ................... 32 

4.2.5 Observations ....................... 36 

4.3 Example-Model Inversion .................... 36 

i 
ii Contents 

4.3.1 Problem Description ................... 37 

4.3.2 The Formal Model .................... 37 

4.3.3 Rule-Based Implementation ............... 38 

4.3.4 Requirements and Validation .............. 39 

4.3.5 Observations ....................... 42 

5 Conclusions and Recommendations 45 

A P-BEST 49 

A.l How P-BEST Works ....................... 49 

A.l.l Facts ............................ 51 

A.1.2 Rule/Fact Bindings ................... 52 

A.2 P-BEST Components ...................... 53 

A.2.1 The Language ...................... 53 

A.2.2 The Compiler ....................... 53 

A.2.3 The Debugger ....................... 54 

B EHDM 55 

B.l The EHDM Specification Language and Logic ......... 55 

B.2 The Theorem Prover of EHDM ................. 56 

B.3 The EHDM Environment ..................... 57 

B.3.1 The Context and Library Manager ........... 58 

B.3.2 The Configuration Control Tool ............. 58 

C Tic-Tac-Toe Rule base 61 

D Tic-Tac-Toe Specifications 75 

arrays ............................... 76 

data ................................ 77 

difh ................................ 78 

facts ................................ 79 

sets ................................. 80 

states ............................... 82 

ttt-ptypes ............................. 83 

ttt-rlsl ............................... 86 

ttt-rls2 ............................... 90 

ttt.rls3 ............................... 94 

ftt.rls4 ............................... 97 

guarded-ops ............................ 100 
Con tents ... 

111 

safe-ttt ............................... 104 

initial-state ............................ 108 

initial-proof ............................ 109 

gwr-proof ............................. 111 

gwc-proof ............................. 113 

gwd.proof ............................. 115 

E Backward-Chaining System 117 

F Heuristics for Electrical System Diagnosis 123 

G Derived Expert System Rules for Diagnosis 127 

H Electrical System Formal Specification 135 

components ............................ 136 

enginemodel ........................... 138 

test ................................. 139 

predict ............................... 140 

Bibliography 145 
Chapter 1 

Introduction 

Almost all computer software harbors faults; those faults can lead to failure, 

and failure can have serious consequences. Stringent measures are (or should 

be) taken to ensure that software faults in critical systems will not lead to 

failurea that could endanger life or national security, cause harm to the 

environment, or have other undesired consequences disproportionate to the 

benefits provided by normal operation. The goal in software development 

for critical systems should be to develop dependuble software-mftware for 

which justifiable reliance can be placed on the quality of service it delivers. 

There are two main approaches for achieving dependability: fault ezclueion, which aims to prevent the occurrence of faults, and fault tolerunce, 

which seeks to detect and recover from the manifestations of faults before 

they can lead to failure.’ Fault exclusion techniques include systematic 

design methodologies intended to prevent faults from being introduced in 

the first place, combined with thorough testing and examination procedures 

intended to identify and eliminate those faults that slip through the first 

stage. Fault tolerance is based on redundancy and run-time checking; because all software faults are design faults, the redundant components cannot 

be simple replicatea of the original, but must be ‘diverse designs” [SI. 

Both fault exclusion and fault tolerance techniques can benefit from the 

observation that dependability is not the same as reliability: it may not be 

necessary to exclude or tolerate all faults, but only those with unacceptable 

consequences [35]. That is to say, dependability can be regarded as reliability 

with respect to unacceptable failures. 

‘What we have called fault exclusion is generally termed fault avoidance; we prefer the 

former term since it haa a more active and positive connotation. 

1 
2 Chapter 1. htroduction 

Dependability requirements for life-critical systems (such as fly-by-wire 

digital control for passenger aircraft) are onerous. For example, the FAA 

requires failures that could endanger a civil aircraft to be “extremely improbable” and “not expected to occur within the total life span of the whole 

fleet of the modeln-the FAA has suggested that this should be interpreted 

as a probability of less than in a 10 hour flight, or lo-’* per hour 

of flight. Substantiating reliabilities such as these through testing is infeasible. Furthermore, experimental and theoretical results cast doubt on the 

failure-independence assumption that underlies the belief that software fault 

tolerance techniques can deliver the required dependability [12,21,32, 371. 

1.1 Formal Verification 

Formal verification is a technique that can, in principle, guarantee the absence of faults. Formal verification demonstrates consistency between two 

different descriptions of a program. Often, one description is the program 

code itself and the other is its specification, although the method can be 

applied equally well to two specifications at different levels of detail. Formal verification treats specifications and programa as formal, mathematical 

texts, and the demonstration of consistency between them takes the form 

of a mathematical proof. Formal verification steps can be “stacked” on top 

of each other, so that a hierarchy of increasingly detailed specifications carries the demonstration of consistency all the way from a highly abstract 

“requirements” statement down to executable code. This guarantees the 

“correctness” of the executable code provided: 

1. The notion of consistency that is employed is appropriate for the intended interpretation. 

2. The requirements statement accurately captures the real (dependability) requirements on the system. 

3. The meaning ascribed to the program code during its verification accurately reflects its behavior during execution. 

4. The proofs are performed without error. 

Consistency is usually equated with logical implication: it is proved that 

the properties of a lower level imply those of the upper one. In other words, 

it is proven that the lower levels do at least that which is specified in the 
1.1. Formal Verification 3 

upper levels. This excludes faults of omission, but not necessarily those of 

commission. 

A requirements statement is just a set of marks on paper; there can 

be no conclusive demonstration that it is an accurate formulation of the 

dependability objectives for the system. The best that can be done is to 

employ notational formalisms that are expressive, precise and perspicuous, 

and to subject the requirements statement to considerable scrutiny. This 

may take the form of testing, either of the requirements specification itself 

(if the specification language is executable), or of a simulation or “rapid 

prototype,” or of analytic scrutiny. The latter can be “formal testing” that 

involves proving conjectures (“if the requirements are right, then I ought to 

be able to prove that the following must be true”), checks for consistency 

and completeness, and informal review. 

The problem of ensuring that the meaning ascribed to a program during its verification (i.e., its formal semantics) accurately reflects its behavior 

during execution (Le., its operational semantics) is a difficult one. One approach is to carry the formal verification down through the specification and 

implementation of the programming language itself, its support software, 

and the hardware on which it runs until the bottom-level assumptions are 

descriptions of elementary logic gates. There has been substantial progress 

recently on each of these levels [8, 14, 15, 30, 39, 401, and some pioneering demonstrations that they can be “stacked.” For the near-term future, 

however, it is reasonable to assume that the correctness of programming 

language implementations will be subject only to informal arguments. 

It is in order to avoid the fourth class of error, errors made during logical 

reasoning, that truly formal, and mechanically assisted, verification is generally recommended. The theorems that need to be proven during verification 

are numerous, massively detailed, and of little intrinsic interest. Experience 

has shown that semiformal proofs, as employed in mathematics journals, are 

unreliable when applied to theorems such as these. Consequently, the use 

of mechanical theorem proving (or proof checking) is attractive. 

The inherent limitations to formal verification identified above are likely 

to be exacerbated in practice by compromises (typically incomplete application, or verification of only limited properties) imposed by technical or 

resource limitations. Nonetheless, formal verification should be considered 

an important component in the demonstration of dependability for critical 

systems, and an even more important component in the process of constructing such systems. When integrated with the design and development 

process (rather than being an after-the-fact analysis), formal verification 
4 Chapter 1. Introduction 

can contribute significantly to the development of dependable systems by 

encouraging systematic and conscious thought, and a preference for simple 

and perspicuous design and implementation. 

1.2 AI Software and Expert Systems 

This report is concerned with the application of formal verification techniques to AI software in general and expert systems in particular. By AI 

software we mean software that uses techniques from the field of Artificial 

Intelligence; Genesereth and Nilsson [24] give an excellent modern introduction to such techniques. Expert systems can be characterized as AI software 

that use highly problem-specific information (as opposed to general laws) 

in order to achieve performance comparable to human specialits in limited 

problem domains. Expert systems employ “surface” rather than ‘deep” formulations of knowledge; they codify empirical associations, special cases, 

and exceptions. These are often expressed in the form of “if-then” production rules, giving rise to the “rule-based expert systems” that are becoming 

widespread. A good survey of expert systems is given by Buchanan and 

Smith [ll]; Harmon and King [28] provide a more elementary overview. 

On the face of it, expert systems seem unlikely candidates for formal 

verification. In the first place, their requirements statements are notoriously 

vague: “build a system to do what Bill does” is not a gross parody of the 

specification for an expert system. Even when requirements are specific, 

they may not be amenable to formal analysis. For example, “build a system 

for loan approval that delivers no more than 4% bad loans by value” is not 

a requirement that can be verified analytically. 

Second, the developmental process used for expert systems is largely 

experimental in nature; the knowledge base is refined “in response to errors 

exhibited in solving test cases” [ll, page 42). The hierarchy of specification 

and design that is the foundation of systematic engineering for conventional 

software, and of its formal verification, is absent for most expert systems. 

As Buchanan and Smith observe [ll, page 471: 

Often when one begins designing an expert system, neither the 

problem nor the knowledge required to solve it is precisely specified. Initial descriptions of the problem are oversimplified, so the 

complexity becomes known only as early versions of the system 

solve simple versions of the problem. Expert systems are said to 

approach competence incrementally. 
1.2. AI Software and Expert Systems 5 

Parnas puts it less sympathetically [43]: 

The rules that one obtains by studying people turn out to be 

inconsistent, incomplete, and inaccurate. Heuristic programs are 

developed by a trial-and-error process in which a new rule is 

added whenever one finds a case that is not handled by the old 

rules. This approach usually yields a program whose behavior is 

poorly understood and hard to predict. 

Third, conventional verification is concerned with algorithmic software. 

The premise of conventional development methodology and of verification 

is that the goal of the exercise is to produce an efficient implementation of 

a systematic method (an algorithm) for satisfying the requirements. Expert 

systems do not satisfy this premise; solutions are found by search rather 

than algorithmically. The knowledge base is not a conventional program, 

but a collection of heuristic information used to guide the search. 

Finally, the languages in which expert systems and their knowledge bases 

are encoded have not been developed with formal analysis in mind. 
Chapter 2 

Requirements and 

Specificat ions 

The absence of precise requirements and specification documents for much 

AI software reflects the genuine difficulty in stating A priori the expectations and requirements for a system whose capabilities will evolve through 

a development process that is partly experimental in nature. However, if 

formal verification is to be applied to AI software, precise requirements and 

specifications are a necessity. We have proposed a possible solution to this 

dilemma in a previous report [48]. 

The basis of our proposal is first to separate the “inherently AI“ aspects 

of AI software from the more conventional aspects-aspects that should be 

amenable to conventional software engineering and quality assurance. To 

this end, we distinguish two sets of requirements and specifications for AI 

software: the competency requirements and the service requirements. 

Competency requirements pertain to those dimensions of the overall requirements that concern “knowledge” or appeal to comparison with human 

skills. We accept that such requirements may of necessity be vague and 

incomplete. Service requirements cover all other requirements and should 

be amenable to statements no less rigorous and formal than those for conventional software. Service requirements should include descriptions of the 

input and output formats expected, the processing rate, the explanation facilities required, and so on. Service requirements and their decomposition 

through levels of specification should be traceable, verifiable, and testable 

just like those of conventional software. 

7 
8 Chapter 2. Requirements and Specifications 

The present investigation is concerned with verification of competency 

requirements. Because we have already conceded that these may be vague 

and incomplete, it may seem contradictory to talk about their formal verification. However, it is not necessary to verify full functional correctness 

in order to accomplish something useful. For many critical applications, it 

is not necessary that the system should not fail, only that it should not 

fail “badly.” Accordingly, we further subdivide competency requirements 

into “desired” and “minimum” requirements. The desired competency requirement will often be defined relative to human expertise and describes 

how well the system is expected to perform. The minimum competency 

requirement, on the other hand, defines how badly it is allowed to perform. 

Whereas desired competency requirements may be hard to state explicitly, there is some hope that minimum competency requirements may sometimes be capable of precise definition. For example, one of the expert systems 

developed at SRI, by the Information Sciences and Technology Division, is 

the Automated Air Load Planning System-MPS [5]. It is used to produce schedules and layouts for loading army divisions and their equipment 

(tanks, helicopters, etc.) onto air transports. One of the things to be considered is the unloading of the aircraft, especially if this is to be performed in 

flight, using parachute drops. As the heavy equipment is first moved around 

inside the aircraft prior to being dropped, and then actually dropped, the 

aerodynamic stability of the aircraft must remain undisturbed. Specifying 

the desired competency of AALPS is obviously difficult-we want a nearoptimum loading plan, but an optimum loading plan is hard to define, and 

it is even harder to determine whether a given plan is optimal. But the 

minimum competency requirement can be given quite a sharp statement: 

the aerodynamic trim of the aircraft must remain within certain limits at 

all times during all stages of unloading in flight. 

We believe that minimum competency requirements may be able to cap 

ture certain desired “safety” properties for AI software and that such requirements can often be cast as formal requirements specifications. In the 

following sections we will look more closely at the formal definition of minimum competency requirements for different classes of AI software. 

2.1 Safety and Liveness Properties 

All extensional properties of programs are conjunctions of safety and liveness properties [4]. A liveness property asserts that something good must 
2.2. CZassification of Expert System Applications 9 

eventually happen; termination is the archetypal liveness property. A safety 

property asserts that some bad thing does not occur during execution. Partial correctness is the archetypal safety property: the “bad thing” that must 

not occur is termination with the wrong answer. The term “safety property” 

is a technical one; such properties need have nothing to do with safety as it 

is commonly interpreted-though we believe that many safety properties in 

the conventional sense of the term can be captured formally by properties 

satisfying its technical sense. 

We can formalize these notions as follows. Let I and 0 be the input and 

output domains of the program P. The input/output behavior of P can then 

be represented by a relation on I x 0: P(i, 0) will be true if execution of P 

can terminate with output o E 0 when given input i E I. P may not be 

intended to work for all possible inputs, so we let V be a predicate on I that 

identifies “valid” inputs. If we now let C be a predicate on 0 that identifies 

outputs satisfying the desired safety property, then the specification that P 

satisfies C for inputs satisfying V is simply:2 

2.2 Classification of Expert System Applications 

Applications of expert systems can be divided into those concerned with 

problems of interpretation (analysis) and those concerned with problems of 

construction (synthesis). Buchanan and Smith [ll, pages 28 and 291 tabulate 

some of the major examples of each kind. Among the most common of 

the analytic systems are those concerned with equipment monitoring, fault 

diagnosis, and the screening and interpretation of data. Expert systems 

for synthesis include those concerned with planning, scheduling, loading 

(MPS is in this category), configuration, and design. We believe that 

another way of looking at this dichotomy between analytic and synthetic 

expert systems sheds more light on their possible requirements specifications. 

Our alternative dichotomy is that between constraint satisfaction and model 

inversion. 

‘We use relationa rather than functions (i.e., we do not write P(i) = 0) to allow the 

‘We uae 1, A, V, and 3 to denote negation, conjunction (“anda), disjunction (“or“), 

possibility of nondeterministic behavior. 

and implication, respectively. 
10 Chapter 2. Requirements and Specifications 

2.2.1 Constraint Sat is fact ion Problems 

A constraint is a predicate over the output variables of a program. The 

constraint satisfaction problem is to find an assignment of values to those 

variables that satisfies the constraint. The important point about constraint 

satisfaction problems is that we can check whether purported solutions do 

indeed satisfy the constraint. Optimization problems are a variation on constraint satisfaction. We want a solution that not only satisfies the constraint, 

but also maximizes (or minimizes) some function. It may not be feasible to 

check whether a purported solution to an optimization problem is indeed op 

timal, but it is at least possible to check whether it satisfies the constraint. 

Often, truly optimal solutions are not necessary; in these cases bounds on 

acceptable values may be characterized as part of the constraint to be satisfied (e.g., “find a loading plan that uses no more than three aircraft”). We 

will call these bounded constraint satisfaction problems. We contend that 

minimum competency requirements for synthetic expert systems can often 

be formulated as bounded constraint satisfaction problems-and specifications for such problems can be formalized as safety properties. For example, 

let P be the AALPS program, U a definition of “valid AALPS input” and 

C a formalization of the constraint “the loading plan places the center of 

gravity of each aircraft within acceptable limits.” Then the simple safety 

property 

vi E I, o E 0, (i) A P(i, 0) 3 c(o) 

expresses the requirement that if UPS is given valid input, and if it 

terminates, then any loading plan produced must place the center of gravity 

of each aircraft within acceptable limits. 

2.2.2 Model Inversion Problems 

A model is a simplified representation or description of a system or complex entity, eipecially one designed to facilitate calculations or predictions” 

(Collins English Dictionary). 

Computer models can range from systems of equations capable of yielding highly accurate and precise numerical predictions (e.g., for orbital mechanics) to descriptions that provide only qualitative information. To qualify 

as a model, a system representation or description should have some explanatory or causal value: it should in some sense describe how the system being 

modeled actually works. A model has much in common with a physical 
2.2. Classification of Expert System Applications 11 

theory, and need not be correct or complete in order to be useful- long 

as its predictions are adequate for their purpose. 

Models have parameters-quantities whose values differ from one instance of the model to another. In the case of a model for an automobile 

electrical system, for example, the parameters might include the voltage at 

the battery, and whether or not the starter motor is broken. Usually, certain parameters can be identified as inputs (i.e., their values are determined 

by factors external to the system being modeled), and others as outputs. 

Inputs can be regarded as ‘causes” and outputs as ‘effects”; the model is 

then a mechanism for reasoning from causes to effects. 

Computer models are often used in this predictive manner: given values 

for the input parameters, the model is used to predict values for the output 

parameters. Such predictions are usually determined by direct calculation 

and are performed by conventional software. 

is what we call the problem of “model inversion.” Whereas problems of 

prediction can usually be solved by direct calculation, problems of model 

inversion must often be solved by search4ifferent values for the input parameters are tried in turn until a configuration is found that leads to a 

prediction matching the observed behavior. Of course, such explicit searching will often be unacceptably slow, so heuristic techniques may be employed 

to perform the search in an “intelligent” manner. Such heuristic techniques 

can be used in two ways: either they can be used in conjunction with the 

explicit model, or they can be used instead of it. In the first case, heuristics 

can be used to suggest values for the input parameters, the output values 

can be computed, and their divergence from those actually observed can 

be used by the heuristics to adjust the input parameters. (Of course, more 

sophisticated arrangements may sometimes be possible, in which the heuristics are more intimately connected to the structure of the model.) In the 

second case, heuristics are used to suggest values for the input values and 

these are accepted without further checks. 

We contend that many, if not most, analytic expert systems can be 

characterized as heuristic model inversion procedures of this second kindexcept that the model that they invert is never constructed explicitly. We 

further contend that the way to produce precise specifications for such expert 

systems is to construct the missing model. 

We can then say that an analytic expert system is consistent with its 

model if the former is an inverse of the latter-that is, if outputs of the 

The inverse problem-that of finding causes that explain observed effects- 
12 Chapter 2. Requirements and Specifications 

expert system, when supplied as inputs to the model, generate predicted 

effects that match those observed. 

This can be expressed formally as follows. Let C and E be the domains 

of “causes” and “effects,” respectively. Let M, a predicate on C x E, be 

an explicit model (from causes to effects), and let P, a predicate on E x C, 

be an expert system (that reasons from effects to causes). Then the expert 

system P is consistent with the model M if 

Vc E C, e E E : P (e, c) 3 M ( c , e ) 

It is easy to construct variationa on this definition. For example, if 2 is a 

relation on effects, with the interpretation that e’ 2 e means the predicted 

effects e’ do not contradict observed effects e, then we can define a weaker 

notion of consistency as follows: 

Vc E C,e E E : P(e,c) 3 3e‘ : M(c, e’) A e’ J e 

We can also say that P is complete with respect to M if 

VcEC,eE E: M(c,e) 3 P(e,c) 

Consider an expert system to diagnose faults’in the electrical subsystem 

of an automobile, for example. This will typically be a rule-based system 

containing rules such as 

if the starter motor turns 

then 

and there is no spark at plugs 

there is a problem in the HT Coil 

An explicit model, on the other hand, would link the components of the 

subsystem in cause-effect relationships in some suitable degree of detail. A 

highly detailed model might account for actual voltage, current, and resistance values, whereas a qualitative model might simply deal with the signs 

(i.e., positive or negative) of various quantities and their derivatives. For 

some diagnostic problems, a simple model of fault propagation is all that is 

needed (i.e., a component fault is assumed to affect all sensors “downstream” 

from that component). A simple model for the automobile electrical system 

might note that the battery is “upstream” from both the starter motor and 

the HT coil, and the HT coil is upstream from the spark plugs. (This sort 

of model is sometimes called a “causal net”). The expert system rule given 

above is consistent with this model. The rule 
2.3. Formal Requirements Specifications 13 

if the starter motor does not turn 

then 

there is a problem in the battery 

is weakly consistent with the model if we define e’ e to mean that the 

observations predicted abnormal in e‘ are a superset of those observed abnormal in e. 

2.2.2.1 Abduct ion 

There are many different representations for the many different types of 

models-differential equations, directed graphs, and predicate calculus, for 

example. In the case of predicate calculus representations, model-inversion 

can be described by a form of logical inference known as “abduction.” Given 

the premise (Vz : P(z) 2 Q(z)), the familiar process of deduction allows us 

to reason from the observation P(a) to the conclusion Q(u). Abduction, on 

the other hand, allows us to reason from the observation Q(a) to the possible 

“explanation” P(u). With a complex model, there can be many abductive 

explanations for a given observation and various criteria have been devised 

for selecting a preferred explanation [52]. 

Abduction has been proposed as a technique for model-based diagnosis [17, 411 and methods for mechanizing abductive inference have been 

developed [16, 45, 521. We believe that abductive techniques can also serve 

to specify minimum competency requirements for certain model inversion 

problems. 

2.3 Formal Requirements Specifications 

We have introduced two classes of problems and shown how formal specifications can be given for each. We contended that constraint satisfaction 

could provide formal specifications for expert systems that perform synthesis 

while model inversion serves that purpose for analytic systems. Of course, 

this dichotomy is a little simplistic: some aspects of analytic expert systems 

may be best specified in terms of constraint satisfaction, while synthetic 

systems may have some model inversion attributes. And some requirements 

may lend themselves to neither constraint satisfaction nor model inversion 

formulations. (For example, planning probably requires the introduction of 
14 Chapter 2. Requirements and Specifications 

a third problem class.) Nonetheless, we believe that our two classes of problem formulation are adequate to specify the requirements of many expert 

system applications. 

The question remains, do our formulations make “good” requirements 

statements? One of the principal characteristics desired of a requirements 

formulation is that it should be comprehensible: those responsible for the 

procurement and quality assurance of a system must be able to scrutinize its 

requirement statement and convince themselves that they truly understand 

its implications and limitations. We believe that the statements that any 

results produced by an expert system are to be consistent with “this set of 

constraints” or “that model” do satisfy this desideratum. A model that provides some plausible and systematic causal connection between inputs and 

outputs is far more comprehensible and defensible-and surely represents 

more “knowledge”-than a set of associations encoded as rules. 

If constraints and models can serve so well as the requirements specifications for expert systems, why do we build rule-based expert systems at 

all? Why not build constraint satisfaction and model inversion procedures? 

We are convinced that the development of such procedures is the correct 

direction to pursue if reliable expert-like systems are to be produced. There 

are, in fact, substantial bodies of work on constraint satisfaction (the book 

by hler [34] is a good introduction) and qualitative modeling (see the book 

edited by Bobrow [lo]). Diagnosis of physical systems is a field in which 

direct model-based procedures have been studied extensively (see biter’s 

work [46], for example, and the survey by Davis and Hamscher [18]). 

In the short term, however, it is likely that expert systems will be able to 

outperform systems based on direct constraint satisfaction or model inversion. For one thing, many problems of interest lack good models (strategic 

warfare and medical diagnosis, for example) and a good ad hoc expert system may be able to do better than a simplistic model or constraint-based 

system. However, we believe that even simplistic models and constraints 

serve to establish useful minimum competency requirements for such expert 

systems. 
Chapter 3 

Languages 

The languages in which expert systems are commonly written, whether 

“rule-based,” “frame-based,” or “object-oriented” have not been developed 

with formal analysis in mind. In particular, they lack formal semantics, and 

generally lack the regularity and conceptual simplicity that would make the 

construction of formal semantics feasible. 

For concreteness, we will use forward-chaining production rule languages 

as our paradigm for languages used in the implementation of expert systems. 

These languages (for example, OPS5 [23]) are appropriate when all input 

data are known in advance, or are easy to collect, and when there are relatively few hypotheses to be explored. Such are likely to be the case in many 

near-term space and aviation applications of expert systems, where input 

data are usually provided by sensors. 

3.1 Declarative Semantics 

There is some similarity between rule-based notations and logic programming languages such as Prolog [13] and OBJ [26]. A pure logic programming 

language (e.g., OBJ) has a declarative semantics: a program can be interpreted as a theory in the logic, and computation is equivalent to deduction 

in that logic. The behavior of programs in execution can be predicted by 

proving theorems within the logic. Impure logic programming languages 

(e.g., Prolog) compromise the declarative semantics in order to improve 

performance and to provide for the deliberate “control” of execution behavior. Thus, most Prolog interpreters omit the “occurs check” (which renders 

them unsound), use depth-first search (which renders them incomplete), add 

15 
16 Chapter 3. Languages 

“negation as failure” (whose logical interpretation is a controversial topic 

[22]), and provide extra-logical “control” constructs such as “cut,” “assert,” 

and “retract.” (Although these features destroy hopes for a declarative semantics, it is possible to give them a denotational semantics [19].) 

Production-rule languages add further control and other features (e.g., 

nonmonotonicity) that take them even further away from pure logic programming languages-and compromise still further any declarative semantics. Buchanan and Smith justify this as follows [ll, page 341: 

Many designers of expert systems are uncomfortable with mathematical logic as a representation language because it lacks expressive power. Numerous extensions must be made to express 

some of the concepts that are frequently used in applications: 

uncertainty, strategy knowledge, and temporal relations. Some 

logicians are uncomfortable with reasoning that is not theorem 

proving and with knowledge bases that are not axiomatic systems 

that allow proofa of consistency and completeness. The search 

for new logical formalisms that are more powerful than predicate 

calculus reflects the tension between simple, well-understood formalisms and expressive power. 

3.2 Operational Semantics 

If the need to consider control strategies and working memory makes the 

search for declarative semantics for rule-based languages rather unpromising, 

perhaps it will be better to consider more operational semantics-that is, 

semantics that explicitly consider the existence of “state” and control flow. 

Hoare introduced a notation and deductive system for reasoning about 

the partial correctness of imperative programs in his seminal paper [29]. 

In this notation, if C is a program, and P and Q are conditions on 

the program variables used in C, then the notation {P}C{Q} expresses the 

safety property that if execution of C begins in a state (i.e., an assignment 

of values to program variables) satisfying P, und if ezeeution terrninutes, 

then it must do so in a state satisfying Q. 

An alternative notation that makes the system state explicit is sometimes 

preferable. In this notation, conditions are modeled as predicates on states 

(assignments of values to program variables), and programs as relations on 

states. If s and t are states, then P(s) is true if state s satisfies condition P, 

and C(s,t) is true if program C, when started in state s, can terminate in 
3.2. Operational Semantics 17 

state t. The connection between the two notations (see, for example, [27]) 

is given by 

{P}c{p} Vs,t : P(s) A C(8,t) 3 a(t) 

‘Proof rules” for the elementary constructs of a programming language, 

together with rules for their combination, allow properties of imperative 

programs to be proved. An example of a proof rule is that for the ‘while” 

loop: 

{P A B}C{P) {P} while 0 do C{P A 70) 

The hypotheses of the rule are written above the line, the conclusions are 

written below it. A formula P such that { P A 0}C{ P} is called an invariant 

of C for 0. 

The difficulty in applying these ideas to production-rule languages is that 

the control structures of production-rule system are less explicit and regular than “while” loops, and the control (Le., conflict resolution) strategies 

used are quasi-nondeterministic. It is possible to give Hoare-style semantics 

for pure nondeterministic constructs (e.g., for Dijkstra’s guarded command 

language [20]’), but the strategies used in production-rule languages are so 

operational that they defy tractable formalization. 

It ia important to understand just how complex some of these control 

features are; a brief description of the operation of OPS5 should make it 

clear. 

OPS5 programs consist of rules called productions, each of which comprises a condition part (called the LHS) and an action part (called the RHS). 

Programs operate on a global database called working memory by repeatedly performing a sequence of actions called the recognize-act cycle: 

Match: evaluate the LHSs of the productions to determine which are satisfied by the current contents of working memory (the set of eligible 

productions so formed is called the conflict set). 

Conflict Resolution: select one production from the conflict set; if the 

conflict set is empty, return control to the user. 

Act: Perform the actions specified in the RHS of the selected production 

(this is called firing the production). 

‘Dijkstra uses .weakest preconditions’ rather than Hoare logic, but the differences 

between these formalisms are not significant to our discussion. 
18 Chapter 3. Languages 

The elementa of the conflict set are called instantiations; they consist of a 

production and a binding of working memory elements to the variables in 

its LHS. The conflict resolution strategy is the following2: 

1. Discard from the conflict set those instantiations that have already 

fired. (The definition of “already fired” is complex; roughly speaking, 

it means that there is some n such that this instantiation has been 

present in every one of the previous n confiict sets, and that it was 

selected for firing in one of those sets.) 

2. Compare the recencies (the cycle on which they last changed) of the 

working memory elements matching the first condition elements in 

each instantiation. Retain those with the most recent elements. 

3. Order the instantiations on the basis of the recencies of the remaining 

working memory elements using the following algorithm to compare 

pairs of instantiations. First compare the most recent elements from 

the two instantiations. If one is more recent than the other, the instantiation with that element dominates. If the two are equally recent, 

compare the second most recent elements from each instantiation, and 

so on, until either a difference is found or one instantiation runs out of 

elements. If one instantiation exhausts its elements before the other, 

the unexhausted instantiation dominates. 

4. If no single instantiation dominates all others under the previous rule, 

use the one with the most conditions in its LHS; if that does not select 

a unique rule, choose one arbitrarily. 

Forgy [23] defends these rules on the grounds that “they make it easy to 

add productions to an existing set and have the productions fire at the right 

time, and because they make it easy to simulate common control constructs 

such as loop and subroutine calls.” Anyone concerned with formal reasoning (or just reasoning) about rule based systems might wish that control 

structures were explicit rather than “easy to simulate.” (The same argument 

applied to imperative programming languages would justify the elimination 

of all control structures except the “goto,” since it can also simulate those 

control structures.) 

Additional conflict resolution strategies that are commonly employed 

include giving preference to rules according to their position in the rule- 

’This is the strategy called MEA; OPS5 ale0 has a strategy called LEx--see 123). 
3.3. Approximate Semantics 19 

base (early rules have preference), or associating explicit priorities with rules 

(rules with high priority have preference). 

3.3 Approximate Semantics 

The inescapable conclusion from the previous two sections is that the construction of either declarative or Hoare-style semantics for current rule-based 

languages is a hopeless task. In the long term, we expect that concern for 

predictability and reliability will lead to the development of programming 

languages with tractable semantics for expert system applications (just as 

it has, to at least some extent, with conventional languages). In the near 

term, however, we either have to accept something less than perfect, or give 

UP. 

Because we have already abandoned the attempt to prove correctness 

for expert systems, being willing to settle instead for proofs of, possibly 

modest, safety properties, it may be that merely “approximate semantics” 

will suffice for our purposes. 

Recall that the (exact) functional behavior of a program P is identified with the relation P(i,o). An approximate semantics will associate a 

somewhat different relation Papprox(i, 0). To be useful, the approximate semantics must be conservative-that is, they must not “underestimate” the 

exact behavior (at least when applied to valid inputs). Thus we require: 

It will then follow that safety properties established with respect to the 

approximate semantics will hold for the exact semantics as well. 

3.3.1 Approximate Declarative Semantics 

We have seen that rule based languages differ from pure logic programming 

languages most violently in providing implicit and explicit control over the 

order in which rules are selected. (The other serious difference is that rulebased languages allow values to be asserted and retracted; we will ignore 

this issue for now.) If there were no conflict resolution strategy-i.e., if any 

and all matching rules could fire-then we would be closer to a purely logical 

interpretation of the rules. Now the effect of conflict resolution strategies is 

to limit which rules can fire-so that fewer things will happen in the presence of conflict resolution than in its absence. This means that a logical 
20 Chapter 3. Languages 

interpretation of a rulebase (i.e., no codict resolution) should indeed provide a conservative approximate semantics. Unfortunately, it will often be 

so conservative that nothing useful can be deduced. An example might help 

make this clear. 

Consider the following rules from a system to handle hospital admissions, 

and suppose that conflict resolution is performed by giving priority to rules 

according to the order in which they appear. 

if head-in j ury(X) 

then 

and time-since-injury(X1 < 8 

send-to(][) := emergency-room 

if can-walk(l0 

then 

send-to(X) := waiting-room 

Now suppose we would like to establish the safety property “anyone who 

has had a head injury within the last 4 hours will be sent to the emergency 

room.” 

Interpreting the rules as a logical theory, we have 

head-injury (X) h time-since-injury(X) < 8 3 send-to(X) = emergencyroom 

can-walk(X) 3 send-to(X) = waiting-room 

It is clear that we can establish our safety property from the first of 

these formulas. However, because there is no ordering implied between the 

formulas when interpreted in logic, “firing” the first does not preclude the 

second one from firing also. Thus, if it happened that patient X was able to 

walk, we might 0l80 conclude that he should be sent to the waiting room. 

In approximating our rule base by a logical theory, we have lost too much 

information. For the conflict resolution strategy considered in this example, 

it is easy to see that the strategy can be encoded in the approximating 

theory: we simply conjoin to the antecedent of each formula the negations 

of the LHSs of earlier rules: 
3.3. Approximate Semantics 21 

head-injury(X) A time-since-injury(X) < 8 3 send-to(X) = emergencyroom 

-t(head-injury(X) A time-since-injury(X) < 8) A can-walk(X) 3 

send-to(X) = waiting-room 

The dynamic nature of most other conflict resolution strategies precludes 

such simple static representations, however. 

Although simply regarding a rule base as a logical theory may provide 

an excessively conservative semantics, it may still be possible to derive some 

benefit from the exercise. Suppose we were to modify the theory by adding 

clauses to the antecedents of its formulas until we were able to prove the 

desired safety properties. This would make explicit the requirements on 

the conflict resolution strategy to be employed-which could be valuable 

information. Informal arguments could then be used to justify the differences 

between the rules and the derived formulas (or the rules could be modified 

to make them less dependent on the conflict resolution strategy). 

Consistency 

There is a flaw in this reasoning, however. If the derived theory is inconsistent, then it can be used to prove any safety property whatsoever. Before 

we proceed to analyze this issue, it will be helpful to review some of the 

notation and terminology of logic. 

A (propositional) theory 7 is simply a set of (propositional) formulas; a 

formula ? is a theorem of 7 if 7 I- ?-that is, if any model of 7 is also a 

model of 7. By the deduction theorem, this is equivalent to I- 7 ZI ?-that 

is, 7 3 ? must be valid (true in all interpretations). If 7 is inconsistent, 

then it has no model (by definition), so all interpretations will valuate 7 to 

false, and hence 7 3 7 to true-whatever formula ? may be. 

It seems, therefore, that we must check any theories derived from rule 

bases for consistency before proceeding to draw any conclusions. In fact, 

the situation is rather more complex than this. For the theory derived from 

a rule base to be consistent simply means that it has a model (i.e., some 

interpretation of its constant, function, and predicate symbols that valuate 

all its formulas to true). However, it may be that the facts initially asserted 

into the working memory of the expert system are inconsistent with any 

models of its rule base. Again, we will be able to prove arbitrary formulas. 

The explanation is, of course, that it is not the rule base alone that induces 
22 Chapter 3. Languages 

the theory corresponding to an expert system-it is the rule base plus the 

initial facts. 

This explains something that others have noted: the notions of inconsistency employed in logic and in rule based expert systems do not coincide. 

In logic, the following set of formulas is consistent 

because both formulas evaluate to true in any interpretation that assigns 

false to p. However, if these formulas are interpreted as rules, and p and 

r are input variables assigned the value true, then both q and iq will be 

asserted-an obvious contradiction. The problem here is that although the 

rules are consistent on their own, they form an inconsistent theory when 

combined with certain initial values. That is, the following “instantiated 

theory” is inconsistent: 

P’Q 

pAr 3 ’q 

P 

r 

This observation allows us to define conektency for the theory corresponding to a rule-based system as follows: let IO be any interpretation for 

the inputs to the system (i.e., assignment of initial values): then there must 

exist a model for the rule base (interpreted as a theory) that is an extension 

to Io. 

Several authors have proposed methods for testing rulebased systems 

for consistency [9, 25, 42,531 but none of them present a rigorous definition 

for rule-base consistency, though Ginsberg I251 does observe that it is different from the notion of consistency in a logical theory (the example above 

is due to him). We therefore believe that ours is the first precise definition of consistency for rule-based systems. It should be possible to use our 

definition to provide a proof of correctness for Ginsberg’s KB-Reduction al81f there ia a validity constraint on input values, then we can restrict the interpretations 

to those that satisfy it. 
3.3. Approximate Semcmtics 23 

gorithm [25].‘ It should also be possible to accommodate the simpler forms 

of nonmonotonic reasoning (such as the closed-world assumption). 

The notion of consistency derived above is a logical one: it simply assures us that there is some way of satisfying the rule base given any (valid) 

assignment of values to the inputs, without assuming a particular conflict 

resolution strategy. The “answer“ produced by the system will be (part of) 

the interpretation that constitutes a model for the rule base. Now there 

may be several models in general, and so several different sets of outputs 

corresponding to the same inputs. This naturally prompts the introduction 

of a second notion for consistency: if the same set of inputs can produce 

several sets of outputs, then it may be desirable in many cases that each of 

these sets of outputs should be “similar” or “consistent” with each other.5 

That is, we should require: 

where N denotes “similarity” (presumably an equivalence relation). 

It is not clear how (or whether) one can verify this property of “output 

consistency” in general; it is similar to “sensitivity” or “continuity”-the requirement that inputs that are close together should generate outputs that 

are also close together. Empirical tests seem the only plausible way to validate such properties.* A property that is sometimes capable of verification is 

the stronger one that the outputs corresponding to any set of inputs should 

be unique. In the case of a rule-based system, this will be so if the order 

in which rules are fired does not deet the final values produced. This lab 

ter property is generally called the Church-Rosser property. Very effective 

testa for the Church-Rower property are known for certain restricted logics (e.g., the Knuth-Bendix procedure [33] for equational theories), together 

with weaker results for more general cases (e.g., [47]). It is possible that 

these techniques also could be adapted to restricted rule bases. 

‘The methods of Suwa et al. [53] and Nguyen et al. [42] are so weak and ad hoc that 

they do not require fnrther investigation. Bezem’s method [9] is simply an algorithm for 

testing whether a particular initial interpretation 10 can be extended to a model for the 

rule base. 

‘This notion of consistency is likely to be particularly appropriate for analytic expert 

syyrtems: how much trust should one place in a system that is capable of producing totally 

different answers from the same inputs? 

‘If the equivalence classes of the similarity relation can be identified with some predicate, then the problem becomes one of constraint satisfaction-which we believe is 

verifiable. 
24 Chapter 3. Languages 

Another property likely to be of some interest is completeness: a rulebased system is incomplete if it can fail to assign a value to some output. 

Analogous to our logical definition of inconsistency, we could say that the 

theory corresponding to a rule base is incomplete if it has models in which 

the interpretation of some output is unconstrained. It seems plausibIe that 

the KB-Reducer algorithm of Ginsberg [25] can be extended to this case. 

We began with the idea that it might be possible to interpret a rule base 

as a logical theory and thereby deduce some approximate, but conservative, 

properties. We have seen that it is necessary to ensure a strong form of 

consistency for the theory so produced. Given such a consistent theory, it 

may then be possible to prove that certain constraints will be satisfied in 

any execution of the system. Performing such a proof might seem to require 

general theorem proving capability. In fact, all the information required 

is gathered as part of Ginsberg’s KEReducer consistency-checking procedure. KB-Reduction is essentially a form of symbolic execution [31]; for 

each ‘hypothesis”, ‘labels” are built up that indicate the combinations of 

input values that will cause that hypothesis to be asserted. The label for 

a hypothesis asserted on the right-hand side of a rule is computed by symbolic evaluation of its left-hand side. For example, if the “partial labels” for 

hypotheses D and A are respectively p V q and p, then the rule D A -A -+ B 

will add 0, v q) A -p (which simplifies to q A ~p) to the label for B. Thus, to 

verify a constraint such as “anyone who has had a head injury within the 

last 4 hours will be sent to the emergency room,” we simply check that the 

label for “being sent to the emergency room” is implied by the condition 

‘head injury within the last 4 hours.” 

It should be perfectly straightforward to develop an implementation of 

Ginsberg’s KEReducer procedure that supports this limited form of verification. It should be noted that there is great similarity between these topics 

and algorithms for rule-based systems and those for decision tables [36, 381. 

3 3.2 

While the investigation of approximate declarative semantics has shed some 

light on the question of consistency, and suggests a way of verifying constraints for elementary rule bases, we believe that approximate imperative 

semantics provides a more suitable base for verifying more complex properties. As with the declarative approach, the more complex forms of conflict 

resolution will not be modeled, but the presence of an explicit state allows 

operational constructs to be modeled more accurately. In particular, the asApproximat e Imperative Semantics 
3.3. Approximate Semantics 25 

signment of values to variables (and subsequent reassignment of new values) 

is easily accommodated. 

The semantics of an individual rule 

ifC then A 

can be modeled by the standard axiom 

{P A C}A{P} {P} if C then A{ P} 

Here the predicate P is an invariant maintained by the rule. If a number of rules all maintain the same invariant, then their nondeterministic 

combination will also maintain that invariant, as will the iteration of that 

combination. 

The basic idea for rule base verification using approximate imperative 

semantics is to establish an invariant for the entire rule base and to verify, 

using the rule above, that it is indeed an invariant for each rule in the rule 

base. If the invariant is also guaranteed true for any valid input, then one 

may conclude that it will be true when the rules terminate. 

It might seem that any formula that is true of the inputs to the system, 

and that is maintained true by all the rules in the system, can only encode a 

very weak property. In a strict sense, this is obviously true, but a great deal 

of information can be encoded in the invariant using control variables. These 

are variables that record and control the progress of computation in the rule 

base. When a rule that initiates a new stage of processing fires, it sets a 

control variable to a particular value to indicate that fact. Some rules will 

condition their LHSs on the values of control variables (e.g., if control-var = 

x and other conditions then actions), so that they are eligible for execution 

only during certain stages of processing. The system invariant can exploit 

this attribute by having different components for different control valuesthat is, it may have the form 

control-var = x 3 invariant-component-x 

A control-var = y 3 invariant-component-y 

A control-var = z 3 invariant-component-z 

Informal arguments will probably have to be used to argue that, on termintion, the control variable will have a value associated with an "interesting" 

component of the invariant. 
26 Chapter 3. Languages 

In the case of constraint satisfaction problems, the constraint will provide 

the invariant, or at least one component of it, to be verified. For model 

inversion problems, the invariant to be verified will be that the components 

of the “answer” being constructed are consistent with the model employed. 

In particular, the rule Vsymptoms then cause” should be supported by the 

argument that in the explicit model, “cause” leads to “symptoms.” The next 

chapter presents a preliminary experimental investigation into the utility of 

these ideas. 
Chapter 4 

Examples 

4.1 Introduction 

In this chapter we report on some of our experiences and observations in 

attempting to apply techniques proposed in this report to the verification of 

rule-based expert systems. The experiments described in this chapter should 

not be considered as indications of our current capabilities; rather, they serve 

to illustrate what we believe to be some of the promising approaches and 

interesting challenges concerned with expert system verification. 

including the P-BEST expert system shell and the EHDM verification environment [55]. P-BEST is a forward-chaining production system that resembles OPS5 [23] and other similar tools. For a more complete description 

of the P-BEST environment, see Appendix A. EHDM is a formal specification and verification environment constructed at SRI. For an introduction 

to EHDM, see Appendix B. 

These experiments were conducted using various notations and formalisms, 

4.2 Example-Const raint Sat isfact ion 

In this section, we consider the application of formal reasoning to the development and verification of constraint-satisfaction type expert systems. The 

example presented here considers the problem of constructing an expert 

system that plays the game 'Tic-Tac-Toe." 

27 
28 Chapter 4. ExmpIes 

4.2.1 Problem Description 

The game of tic-tac-toe may be thought of as a constraint satisfaction problem. Given an arbitrary legal board configuration, the computer is required 

to place a marker in a position such that a certain goal is achieved. We 

considered the ‘classical” two-player version of tic-tac-toe as played on a 

3x3 board (illustrated in Figure 4.1). The goal of the game is to place three 

Figure 4.1: Tic-tac-toe Board Configuration 

markers on the board so that they are in alignment either vertically, horizontally, or diagonally, while preventing the opponent from placing three 

markers in alignment. Play begins with an empty board, and proceeds as 

alternating players place markers on the board until either: (a) some player 

achieves the placement of three markers in a row, or (b) no remaining empty 

positions exist. 

4.2.2 Rule-Based Implementation 

We implemented an initial rule base to play tic-tac-toe. To further constrain 

the problem, we adopted the convention that the opponent would always get 

the first move. In an effort to model the process of knowledge engineering, 

in which insight into the problem space is gathered in a piecewise fashion, 

we adopted a naive playing strategy that can be informally stated as follows: 

0 If the computer can win (i.e., place a marker 80 that there are three 

markers in a row, either vertically, horizontally, or diagonally), then 

have the computer place the marker in the winning position and terminate the game. 

0 If the computer must block to prevent the opponent from winning, 

then have the computer place a marker in the blocking position. 

0 Otherwise, have the computer place a marker in one of the following 

positions, arranged according to desirability: center, corner, middle. 
4.2. Exampleconstraint Satisfaction 29 

Using P-BEST, a forward-chaining expert system shell, we defined the 

following fact templates. In P-BEST, a fact template must be declared for 

each possible assertion. In the case of the tic-tac-toe example, there were 

three possible types of assertions that could be made into the knowledge 

base: 

0 position assertions 

0 turn assertions 

0 opponent move assertions 

Position assertions were used to represent the state of the playing board 

at any given point during the game. There were exactly nine such assertions 

at all times-one assertion for each of the nine possible positions on the 

playing board. At the beginning of play, each of these assertions contained 

the designation that the corresponding position was free of any marker. As 

play progressed, the position assertions were altered to reflect when a marker 

was placed in the corresponding location. Such markers were designated as 

“opp” short for opponent, and ‘com” for computer. 

Turn assertions were used to record whose turn it was at any given point 

in the game and to keep track of how many turns had transpired. 

Opponent-move assertions were used to communicate the intention of the 

human opponent to the knowledge base. Incorporated into the knowledge 

base were several rules that were responsible for querying for the opponent’s 

move, checking its legality, and asserting A proper opponent-move assertion 

into the knowledge base. Because these rules do not effect the behavior of the 

program with respect to its strategic performance, they are not considered 

in the subsequent analysis. 

Figure 4.2, gives an example of what the declaration of these fact templates, called “ptypes” or predicute-type8 in the terminology of P-BEST, 

looks like. For a more complete description of the P-BEST system, see 

Appendix A. 

For an example of the syntax of the P-BEST rules, refer to Figure 4.3, 

which gives an example of the rule “makeiandommove” from the tic-tac-toe 

rule base. This rule is given an explicit ranking, in this case -10, whit& affects 

the selection of which rule to execute when there are multiple candidates. 

The higher the rank of the rule, the greater priority given that rule during 

conflict resolution. The effect of this rule is that when it is the computer’s 

turn to move, if no rules with higher ranks are eligible to fire and if there is 
30 Chapter 4. Examples 

(define-ptype POSITION 

'A unique pouition in the 3x3 board.' 

row 

col 

marker 

; integer - range 1 to 3. 

; integer - range 1 to 3. 

; free, corn or opp. 

1 

Figure 4.2: P-type Fact Template Declaration in P-BEST 

a free position left on the board, the computer will select one of those free 

positions and replace the "free" designation with its marker, 'corn". 

The completed initial rule base consisted of 11 rules: 

0 3 rules to detect a condition where the computer can win 

0 3 rules to detect a position where the computer muat block 

0 2 rules to recognize lost and tie games 

0 2 rules to get and check human input 

0 1 rule to make a random move as a default case 

plus a handful of LISP functions that assisted in managing the display of the 

game board. The complete code for the rule base is given in Appendix C. 

4.2.3 Requirements 

Although it is sometimes quite difficult to identify expectation for a system 

whose capabilities will evolve through a developmental process, in order to 

validate the system, either through testing or through formal analysis, it is 

imperative that the requirements against which the system is to be evaluated 

be made explicit. 

Tic-tac-toe can be viewed as an optimization problem; given a board 

position, the computer is expected to pick the beat move possible. Optimally, 

we would like to have a system which wins; however, in this particular game 

it is a well-known fact that a win cannot be guaranteed. A win occurs 

only when the opponent makes a mistake; if no mistake is made by either 

player, the game terminates in a draw. Therefore, a desired competency 

requirement, which is also a liveness property for this system, might be: 
4.2. Example-constraint Satisfaction 31 

(defrule MAKE-RANDOMMOVE 

“Select a paeudo-random porition to place marker. 

Priorithe positions as: 1. center, 2. comem 

and 3. middles.m 

at rank -10 states 

if there exists a turn called tl 

such that player is com and 

there exists a position called pl 

count is ?x and 

such that marker is free 

forget tl and 

remember a position 

then forget pl and 

which inherits from pl 

except that marker is com and 

remember a turn 

such that player is opp and 

count equals (1+ ?x)) 

Figure 4.3: Rule make-randommove From the Tic-Tac-Toe Rule Set. 

0 The system wins, when possible. 

This implicitly includes the notion of playing to the standards of a human 

player; it implies that a strategy is pursued that encourages the opponent 

to make an error, and recognizes such situations in order to capitalize on 

mistakes and force a win. Such a notion would be very difficult to capture 

formally or to check with formal analysis. Even in the game of tic-tac-toe, 

which has limited number of possible system states, an optimal move in 

an arbitrary configuration would be difficult to recognize; in some sense it 

would involve recognizing the strategy of the opponent which may not be 

deducible from the board configuration alone. 

A minimum competency requirement, which is also a safety requirement 

for this system, is somewhat more tractable; above all: 

0 The system shouldn’t lose. 

We have already noted that it is impossible for an opponent to force a win; 

therefore, the minimum competency we required of our system was that it 

never make a mistake that would result in the opponent’s winning. 
32 Chapter 4. Examples 

To formalize this minimum competency requirement, we introduced the 

notion of a safe state. We defined a safe state, which is expressed in terms 

of board configurations, to be those configurations in which the computer 

has won the game, or in which the opponent cannot win the game with the 

placement of the opponent’s next marker. In the language of EHDM, this is 

expressed as: 

safedef: Axiom 

safe(kbx, an) 

won_game(kbx, sn) 

v -dosenextmove(kbx, sn) 

Under our initial formulation of rules, there was no reason to believe the 

expert system should be able to win a game of tic-tac-toe because it does 

not attempt to pursue a winning strategy (the computer simply selects a 

pseuderandom move when it cannot immediately win and need not block). 

However, it was reasonable, to hope that the computer would not lose under this strategy. Specifically, three rules were included in the rule base, 

blkrow, blkxol, and blk-dia, that prevent the opponent from placing a 

marker in any row, column or diagonal which would result in a lost game. 

4.2.4 Formal Specification 

We constructed a formal specification of the tic-tac-toe rule base and proposed to verify that specification against the minimum competency requirement that the system must not lose the game. The specifications for the 

tic-tac-toe rule base are contained in Appendix D. In order to create a 

formal specification for this application, it was necessary first to define an 

approximate semantics for the language of our expert system shell, P-BEST. 

We expressed the nonmonotonicity of the rules by introducing an explicit 

notion of system state. As explained in Section 3.3, one way to accomplish 

this in the EHDM language is to add to value-returning functions an extra 

parameter that corresponds to a specific system state. For example, one of 

the modules in the specification describes a formal object called a kb, which 

is declared to be a set of facts (see module kbs in Appendix D). A function, 

kblnst, of two parameters is provided to access the value of objects of this 

type; one parameter is the knowledge base for which to return the value; 

the other is the current system state. Therefore, the declaration for this 

function in the language of EHDM is: 
4.2. Example-Constraint Satisfaction 

kb-inst: functiona[kb, state + set[fact]] 

33 

With this formulation, we can express that facts that are associated with a 

given knowledge base in a given state may possibly not be associated with 

that knowledge base (i.e., may have been retracted) in some later state, 

without the danger of such retractions leading to logical contradictions. 

Each fact template, or ptype, declaration in the rule base becomes a type 

declaration in the formal specification. For instance, the type position is 

declared to be a subtype of type fact. This allows the declaration and 

use of logical variables that range over all possible positions. Along with 

the type declaration, a function is defined that tests for membership of a 

certain class of instances of a fact in a knowledge base at a particular state. 

With these declarations, a relatively straightforward translation of the rules 

into a logical notation can occur. This can be seen by comparing any of 

the rules in Appendix C with their corresponding formal specifications in 

Appendix D. 

The proof strategy for establishing that the system conforms to the specification of our safety property involves simple induction over all valid sequences of moves. In such a scheme, the initial state of the system, in which 

no markers have been placed on the board, is shown to conform to the prop 

erty in question. In this case, the proof of the safety of the initial state 

is trivial; since there are no markers on the board, there is no way for the 

opponent to win on the next move. Then, given an arbitrary “reachable” 

state that preserves the safety property, if one can establish that all reachable next states also preserve the property, by appealing to induction one 

has established that the property is maintained over all valid sequences of 

moves. 

Figure 4.4: Example Configuration 

In attempting to construct the proof, it soon became apparent that it 

waa impossible to prove the safety property without considering the implicit 

control flow in the rule base and the sensitivity of the operational semantics 

to the ordering of assertions. In the tic-tac-toe rule base, for example, the 
34 Chapter 4. Examples 

rules dealing with blocking the opponent have prekedence over the rule for 

placing the computer’s marker at random. In a situation such as that shown 

in Figure 4.4, where the opponent’s markers are represented as “0” and the 

computer’s markers are represented by “X”, it cannot be proved that the 

computer will not lose on the next move (one of the criteria for the safety 

property in question) if the computer places its marker in any position other 

than row 2, column 1. This is a direct reflection of the fact that it is unsafe to 

execute any rule in the above situation except the rule that explicitly deals 

with blocking an opponent’s win on any particular column; however, if the 

rules are treated as being nondeterministically selected for execution, this 

crucial piece of knowledge is missing and it is impossible to reason formally 

about the safety of the system. 

The informal operational semantics of the tic-tac-toe rule base include a 

ranking of rules. This ranking will prevent the make-randommove rule from 

firing when one of the blocking rules is also a candidate. Since exactly one 

rule fires per state transition, it is operationally impossible for the wrong 

rule to fire. We needed to find a formalism that could capture this implicit 

proceduralism of the rule base. 

Making use of the concept of guarded commands as put forward by 

Dijkstra [20], we adopted a formulation that approximates the proceduralism 

of this application. To do this, we defined a set of operations, one for 

each of the rules, such that the precondition of each operation consisted 

of the conjunction of the negation of the preconditions of all operations of 

higher precedence with the precondition of the corresponding rule. This is 

illustrated in the module guarded-ops in Appendix D. This is only an 

approximation of the actual operational proceduralism because it results in 

a strict ordering of the rules; the actual rule base is only ordered with respect 

to groups of rules at differing precedence levels-rules within each group are 

nondetenninietically selected. However, this strict ordering is suflicient to 

establish the safety property in question. 

The operational semantics of the rule base is also sensitive to the order in which facts are asserted into the knowledge base. For example, the 

make-randommove rule (Figure 4.3) selects a free space to place a marker. 

Contrary to what the name of the rule suggests, the choice of free space is 

not random, but totally deterministic. AB the documentation of the rule 

suggests, the center is always chosen if it is free, followed by the comers (beginning with the upper-right-hand corner and proceeding clockwise), and 

finally by the middles. This precedence occurs because the conflict resolution strategy of P-BEST gives priority to rule instances which reference the 
4.2. ExampbConstraint Satisfaction 35 

most recently-asserted facts. In order to capture this operational dependence 

upon the ordering of the initial assertions, additional axioms were introduced 

to make this ordering available during formal reasoning (see module ttt-rlsl 

in Appendix D). 

The proof attempt uncovered four configurations of the board which 

could result in the computer being forced into a no-win situation; these configurations occur when the opponent can win in two possible ways, making 

it impossible for the computer to block the opponent in a single move. One 

such configuration is illustrated in Figure 4.5. We were able to prove that the 

01 I x 

Figure 4.5: No-Win Sample Configuration 

strategy of the tic-tac-toe rule base prevented the opponent from reaching 

two of these states. However, the formal analysis showed that the remaining 

two configurations could be reached and could cause a loss. Because of the 

existence of these situations, it was impossible to prove the safety invariant 

for the blocking rules as they were originally formulated. In other words, 

our original rule base was incorrect; it failed to consider situations which 

were both reachable and contradictory to our safety requirement. 

With this insight, we were able to expand the definitions of our safety 

requirement to be: 

safedef: Horn 

safe(kbx, an) 

wongame(kbx, an) 

V -(losenextmove(kbx, an) 

V unsafexonfig-l(kbx, an) 

V unsafe_config2(kbx, an) 

~unsafe_config8(kbx, ~~)V~n~afe-~0nfig-4(kb~, sn)) 

To correct the rule base, two additional blocking rules were added at a higher 

priority with respect to the other blocking rules; these rules specifically 
36 Chapter 4. Examph?~ 

countered the two remaining unsafe situations. With the addition of these 

two rules, the inclusion of their logical equivalents in the formal specification, 

and the expanded safety definition, it was possible for the proofs to be carried 

forward. Samples of proofs in the methodology of EHDM are included at 

the back of Appendix D. We did not attempt to complete all proofs; it was 

not necessary to formally complete all the proofs, nor to prove the induction 

hypothesis, in order to derive the benefits of the formal analysis. 

4.2.5 Observations 

From this experiment, we are able to draw the following conclusions. 

The translation of expert system rules into logic requires a formulation 

that captures the state-dependent nature of the inference engine. An approximate semantics for rule-based systems can be formulated which provides an 

adequate framework for reasoning formally about some of the behavior of 

the system. 

While it may be possible to establish very weak invariants independent 

of the conflict resolution strategies involved in the expert system, and independent of the inherent proceduralism involved, it would be impossible to 

establish many important safety properties, such as the one defined for this 

example system, without capturing the implicit control flow. 

Reasoning formally about this application uncovered critical situations 

that were originally overlooked. While the rule base was not incomplete 

or inconsistent according to syntactic analysis, the original rule base was 

incorrect, because it was conceptually incomplete for a class of situations 

that could have led to violation of the safety property during operation. 

Such conceptud incompleteness would not have been discovered through 

any form of syntactic analysis of the rule base. 

4.3 Example-Model Inversion 

In this section we consider the application of formal reasoning to the develop 

ment and verification of model-inversion type expert systems. The example 

presented here considers the problem of constructing an expert system to 

diagnose problems in a car’s electrical system. 
4.3. Example-Model Inversion 37 

4.3.1 Problem Description 

As in all diagnosis systems, the goal of our example program is to be able 

to identify the most-likely cause of a problem given a set of observed effects. 

To constrain the problem, we consider only a simplified subset of an actual 

electrical system. Our subset consists of the following components: 

0 battery cells 

0 battery 

0 ignition switch 

0 points 

0 coil 

0 distributor 

plugs 

0 solenoid 

0 starter 

We limit the set of potential causes to be the set of failed components. 

In other words, we would consider the failure of the ignition switch to be 

a potential cause for the observation that power is failing to be delivered 

to the points and starter solenoid, but we would not consider the state of 

the wires connecting these components as potential sources of the problem. 

Further, we consider only single points of failure in this exercise-for any 

given set of observations, the expert system is required to find the single 

most-probable cause which accounts for the observations. 

4.3.2 The Formal Model 

We created a formal model of our simplified automotive electrical system 

in the language of EHDM; this model is contained in modules components 

and enginemodel in Appendix H. The focal point of this model is the axiom electricalsystemmodel shown in Figure 4.6. The accuracy of this 

formalization is based on a number of assumptions (e.g., the fact that the 

car in question is not running); however, the model is adequate for the illustrative purposes of this discussion. The model asserts that there is a causal 

relationship between various components of the system. To have power at 

the ignition switch, for example, the model states that it is necessary that 

the battery be in a good state of repair and that the battery be delivering 
38 Chapter 4. Examples 

electricabyatemmodel: Axiom 

(power-at(battery) # good(cells)) 

A (power-at(ignition) * powerat(battery) A good(battery)) 

A (power-at(pobts) ++ power-at(ignition) A good(ignition)) 

A (power-at(coil) ++ power-at(pobta) A good(points)) 

A (power-at(distributor) power-at(coil) A good(coil)) 

A (power-at(p1ugs) power,at(distributor) A good(distributor)) 

A (power-at(so1enoid) power-at(ignition) A good(ignition)) 

A (power-at(starter) * power-at(so1enoid) A good(eo1enoid)) 

Figure 4.6: Model of Simplified Automotive Electrical System 

power. This is representative of the fact that the battery is “upstream” 

from the ignition in our simple model, just as the ignition is upstream from 

both the points and the starter solenoid. 

4.3.3 Rule-Based Implement at ion 

For this experiment, we developed a small backward-chaining rule interpreter, which & a variation on Winston’s expert problem solver [56]. Backwardchaining systems start with an unconfirmed hypothesis and attempt to confirm it. This involves identifying rules that subetantiate the hypothesis, and 

then attempting to verify the conditions upon which the applicable rules are 

dependent. Apart from some syntactic sugar in the form of extensions to 

simplify the expression of rules and hypothesis, there are two major differences between Winston’s original system and our enhanced version: 

1. Our system allows the appearance of “not” clauses in the LHS of rules 

2. Our system allows the specification of questions to be used to obtain 

observations from the user, rather than attempting to synthesize such 

questions from the symbolic representation of the facts 

We created two separate implementations of this rule base. One implementation was distilled from a set of troubleshooting and diagnosis procedures contained in Chilton’s Import Car Repair Manual [54]. We would 

expect the quality of this rule base to approximate the results of most standard knowledge engineering efforts. A subset of the rule base is given in Ap 

pendix F. The other implementation was derived from the abstract model 
4.3. Example-Model Inversion 39 

of our simplified system through a relatively mechanical process. This rule 

base is given in Appendix G. 

The procedure for generating the rule base from the axiomatic specification of the model, as seen in Figure 4.6, was straightforward. For each 

equivalence relation specified by the model, a rule is generated to capture 

the equivalence. For example, the relation 

(power-at(starter) e, powerat(so1enoid) h good(so1enoid)) 

caused the following rule to be included in the rule base: 

(def he-rule d7 

(if (power at solenoid) 

(good solenoid) ) 

(then (power at starter) 1) 

Then, rules were provided which define the possible observations and provide questions that may be asked of the user to acquire information about 

the observations. Finally, a set of rules were added which identified the 

global dependencies in the system; these rules serve to associate the failure 

hypothesis with the observations about system behavior. 

4.3.4 Requirements and Validation 

As suggested in Section 2.2.2, requirements for expert systems which have 

formal models can be expressed as 

Vc E C, e E E : P(e, c) 3 M(c, e) 

where C is the set of all causes, and E is the set of effects. This leads to 

a procedure for validating the operation of the expert system against the 

expectations of the model for any given set of causes and effects. 

Our simplified model identifies eight possible causes for the system to 

fail; these eight causes correspond to the failure of one of the eight system 

components. The effects in our model are limited to an observation of where 

power is available and where it is not. There is an assumption that the failure 

of a particular component causes the flow of power through that component 

to cease, making the power unavailable to all components down-stream from 

the failing component, and that the presence or absence of such power is 

observable. What we were interested in showing was, that given a certain 
40 Chapter 4. Examples 

set of observations presented to the expert system, an answer would be 

produced which, when presented to the model, would cause the correct set 

of effects to be predicted. 

To allow the model to be used to make such predictions, we defined two 

additional EHDM modules, test and predict (see Appendix H), which we 

used to predict the values of the observable effects. To establish which effects 

should be observable according to the model, we set the constant comp in 

module predict to the value of the failed component. We then attempted to 

prove eight lemmas, each of which assert that power will be visible flowing 

through a particular system component. The proofs of these lemmas are 

derivable from the characteristics of the model, the value of comp, and the 

assumption that there is a single point of failure. Those lemmas for which 

the proof succeeds correspond to the set of predicted effects. 

Consider the example of a failed ignition switch. To select the set of 

components through which the model predicts power will flow, we set 

comp = ignition 

and invoke the EHDM provemodule command. The results of this command 

is shown in Figure 4.7. In this case, the model predicted that there would 

Proof summary for module predict 

power-at-star 

power-at-sole 

power-at-plug 

power-at-dist 

power-at-coil 

power-at -pain 

power-at Agni 

power-at-batt 

UNPROVED 

UNPROVED 

UNPROVED 

UNPROVED 

UNPROVED 

UNPROVED 

PROVED 

PROVED 

Totals: 8 proofs, 8 attempted, 2 succeeded. 

Figure 4.7: Result of EHDM ProveModule With comp=ignition 

be observable power through the battery and the ignition. To validate the 

expert system, we simply answer the questions which correspond to a faulty 

ignition switch. A transcript of the results of the expert system run is 
4.3. Example-Model Inversion 41 

shown in Figure 4.8. As can be seen from comparing the transcript of the 

Does your car fail to start? (Yes or No) yes 

Does the starter fail to turn when the hey is 

engaged? (Yes or No) yes 

Are all of the voltage levels of the individual 

battery cells normal? (Yes or No) yes 

Rule <DIA> 

Rule <Dl> 

deduces: (GOOD CELLS) 

deduces: (POWER AT BATTERY) 

Are there any cracks or damage to the battery 

cane? (Yes or No) no 

Are the battery posts and cable clamps 

corroded? (Yes or No) no 

Rule <DU> 

Rule <D2> 

deduces : (GOOD BATTERY) 

deduces: (POWER AT IGNITION) 

Does a voltmeter connected to the starter poet 

of the solenoid fail to Rove when the hey is 

turned to the start position? (Yes or No) yes 

Rule <Y6> 

deduces : (BAD IGNITION) 

Diagnosis : BAD IGNITION. 

Figure 4.8: Example Transcript From Expert System 

expert system session with the results of the formal proof, the model and 

the expert system share an inverse relationship. The model was able to 

accurately predict the set of observations consistent with a failed ignition 

switch, and the expert system was able to correctly deduce that the ignition 

switch had failed (while making intermediate deductions consistent with the 

predictions of the model). 
42 Chapter 4. Examples 

It is interesting to note that the expert system may not actually observe 

all of the predicted good components on its way to diagnosing a failure. For 

instance, in the case of a failed solenoid, the model's predictions are shown 

in Figure 4.9. The model predicts that there will be power throughout 

Proof summary for module predict 

power-at-star 

power-at-sole 

power-at-plug 

power-at-dist 

power-at-coil 

power-at ,pain 

power-at-igni 

power-at-batt 

UNPROVED 

PROVED 

PROVED 

PROVED 

PROVED 

PROVED 

PROVED 

PROVED 

Totals: 8 proofs, 8 attempted, 7 succeeded. 

Figure 4.9: Result of EHDM ProveModule With comp=solenoid 

all system components with the single exception of the starter. The expert 

system, on the other hand, on its way to finding the correct answer, observed 

only three of the predicted seven good components, as can been seen from 

the transcript included in Figure 4.10. This is illustrative of the notion of 

weaker consistency as explained in Section 2.2.2. In this case, the 7 in 

Vc E C, e E E : P(e, c) 2 3 e' : M(c, e') A e' 2 e 

corresponds to the relation that the observed effects do not contradict the 

predicted effects and that the predicted effects are a superset of the observed 

effects. 

4.3.5 Observations 

Based on this and other similar experiments, we make the following observations and conclusions. 

Development of the initial rules based upon heuristics was a tedious and 

arduous process which left us feeling very unsure about the quality and 

completeness of the rule base for even so small an example as the one under 

consideration here. Quite to the contrary, we found generation of diagnostic 
4.3. Example-Model hversion 43 

rules based upon an explicit representation of the model of system behavior 

to be a relatively straightforward process. Further, because we were working 

from an explicit model, we felt a much higher degree of confidence concerning the quality of the ensuing rule base. It should be possible to develop 

mechanical translators which are capable of doing much of the transformation from the logical notation used in expressing models to a rule-based 

representation, thereby reducing development costs and further increasing 

confidence that errors were not introduced during the transformation process. 

We believe that the notion of model inversion has great potential for 

application to verification of diagnostic expert systems. While the ideas set 

forward here are still in a formative stage, the success experienced to date has 

left us feeling optimistic about the feasibility of developing verification and 

validation techniques that are both effective and well-grounded in theory. 
44 Chapter 4. Examples 

Does your car fail to start? (Yes or No) yes 

Does the starter fail to turn when the key is 

engaged? (Yes or No) yes 

Are all of the voltage levels of the individual 

battery cells normal? (Yes or No) yes 

Rule <DlA> 

Rule <D1> 

deduces: (GOOD CELLS) 

deduces: (POWER AT BATTERY) 

Are there any cracks or damage to the battery 

case? (Yes or No) no 

Are the battery posts and cable clamps corroded? 

(Yea or No) no 

Rule <D2A> 

Rule <D2> 

deduces: (GOOD BATTERY) 

deduces: (POWER AT IGNITION) 

Does a voltmeter connected to the starter post of 

the solenoid fail to move when the key is turned 

to the start position? (Yes or No) no 

Does the needle of a voltmeter flicker when the key 

is jiggled? (Yes or No) no 

Rule <D3A> 

Rule <DS> 

Rule <D3> 

deduces : (GOOD IGNITION) 

deduces: (POWER AT POINTS) 

deduces: (POWER AT SOLENOID) 

Does the starter buzz or turn the engine slowly when 

a jumper is connected between the battery and starter 

posts of the Solenoid? (Yes or No) no 

Does the starter show no response vhen a jumper is 

connected between the battery and starter posts of 

the solenoid? (Yes or No) yes 

Rule <YQ> 

deduces: (BAD SOLENOID) 

Diagnosis: BAD SOLENOID. 

Figure 4.10: Example Transcript From Expert System 
Chapter 5 

Conclusions and 

Recommendations 

Formal verification is not a technique to be used in isolation: it should be 

a component of a comprehensive development methodology based on the 

systematic application of formal methods. Due to the cost and difficulty 

of applying such methodologies, they are usually reserved for very critical 

applications, where assured reliability and safety are paramount, and where 

simple and robust designs, conducive to formal analysis, may take precedence over functionality. For formal verification to be tractable, and its 

results credible, formal analysis must be part of the design process from the 

beginning and must influence the design as it evolves. 

These are not attributes of expert system development and knowledge 

engineering as commonly practiced today. Consequently, formal verification 

has only limited applicability, and possibly even less utility, in contemporary 

expert systems development. This is emphatically not to say that formal 

verification has no part to play in the development of high-quality expert 

systems, but to point out that much more needs to be done besides develop 

ment of the formal verification techniques themselves. It will be necessary 

to revise much of the practice of expert systems engineering, and some of 

its goals, in order to accommodate requirements for high reliability and 

predictable behavior assured by formal analysis. 

We do not expect-or even advocate-that the field of expert systems 

should confess error and change its working practices and philosophical foundations. Rather, we suggest the creation of a subdiscipline that will seek 

to develop and apply, from expert systems engineering, the methods and 

45 
46 Chapter 5. Conclusions and Recommendations 

insights that are applicable and beneficial to systems with exacting dependability requirements. Formal methods and verification should be a significant technical component of that subdiscipline-which should bear a similar 

relationship to its parent field as the engineering of conventional computer 

systems for lifecritical applications does to the general field of computer 

and software engineering. 

We believe this report makes three contributions to the development of 

a foundation for the subdiscipline of dependable expert systems: 

0 The identification of constraint satisfaction and model inversion as formal specification paradigms for synthetic and analytic expert systems, 

respectively. 

0 A formal definition of consistency for rule-based expert systems. 

0 Identification of the notion of approximate semantics, and examples 

of how these can be achieved and applied in both declarative and 

imperative forms. 

Recommendations for Further Research 

We suggest that research and development should continue on the following 

three levels of increasing rigor and formality: 

1. The development of formally based analysis and anomaly detection 

tools-such as consistency checkers-that can provide useful, but not 

definitive, help in the construction and quality assurance of conventional expert systems. 

2. The development of a methodology and tools for the creation of dependable expert systems, based on formal specifications, run-time 

checking, and fault-tolerance techniques. Constraint satisfaction and 

model inversion can provide not only formal specifications for expert 

systems, but executable tests for the satisfaction of those specifications. By testing the output of an expert system against its specification at run time, and invoking fault-recovery and tolerance mechanisms on failure (e.g., the execution of alternate subsystems or algorithms as in the recovery block method for software fault tolerance), 

it should be possible to develop highly dependable expert systems for 

certain, perhaps limited, applications without requiring a complete 
47 

change in the development and implementation strategy for the expert systems themselves. 

3. The development of a formally-based methodology and tools for expert systems. This will require development of a systematic design 

methodology for expert systems in which knowledge engineering is 

combined with the systematic, topdown elaboration of requirements 

and specifications. It will also require development, for expert systems, 

of programming languages that are amenable to formal analysis. One 

slightly radical, but very promising, approach will be to abandon conventionally hand-crafted, rule-based expert systems for certain critical 

applications, and instead to develop those applications through explicit 

constraint satisfaction and model inversion techniques. The latter may 

involve either the exploration of an explicit model at run time, or the 

“compilation” of that model into an efficient set of production rules. 

Pearce [44] has demonstrated that this technique can be both more 

efficient and more reliable than a hand-crafted rule set. 

We suggest that exploration of the second and third approaches identified above should be conducted and evaluated through modest prototyping 

experiments using potential applications of expert systems of interest to 

NASA and Space Station planners. Fault diagnosis (analysis) and scheduling (synthesis) seem to be the most promising applications, from both the 

scientific and practical points of view. 
48 Chapter 5. Conclusions and Recommendations 
Appendix A 

P-Best 

The Production-Based Expert System Toolset (P- BEST) is a forward-chaining, 

LISP-based expert system development environment (sometimes referred to 

as a shell), which consists of a rule-development language, rule compiler, 

run time routines, and a debugger. It provides an integrated set of facilities 

for the creation and debugging of complex knowledge bases. Although developed primarily as a research vehicle in the exploration of expert systems, 

its features and facilities have been heavily influenced by the suggestions, 

critiques and demands of individuals involved in the applications of expert 

systems to real-world problems. P-BEST is intended to be portable, yet 

reasonably efficient in executing complex rules against large data sets. 

A.l How P-BEST Works 

The basic P-BEST strategy revolves around maintenance of an expert system state. The system state is represented by the union of the states of the 

fact base, the rule base, and any external data structures unique to a given 

application. This union is referred to as the knowledge base (KB). Rules 

(IF. . . THEN. . . pairs) are developed by the user and compiled by P-BEST 

into the rule base. A very simple rule might say something like: 

if is-a-man socrates, 

then 

is-mortal socrates. 

Once the rules are developed, the user may introduce facts (knowledge) into 

the KB through assertions. For example, a user might wish to assert that 

49 
50 Appendix A. P - BEST 

is-a-man socrates 

The P-BEST inference engine is a distributed mechanism for matching 

facts to rule antecedent patterns, performing binding analysis, and invoking 

rule consequents. It is distributed in the sense that for each rule in the rule 

base, the compiler will produce a number of primitive LISP functions that 

implement the semantics of the rule. As facts are asserted, each rule in 

the rule base that references the type of knowledge being asserted examines 

the fact for a potential match. When a pattern in the antecedent of a rule 

matches the fact being asserted, a binding is created and associated with 

both the fact and the rule. If such a binding is created, and if, as a result 

of this binding, all the patterns of a rule have been matched, then binding 

analysis is performed to determine if all of the variable values referenced by 

the rule/fact bindings are consistent. 

Given the example rule stated above, if the fact were asserted 

is-a-man socrates 

then the rule would determine that its antecedent had been satisfied. Because the sample does not specify any additional constraints, the rule would 

pass consistency analysis and conclude that 

is-mortal socrates 

Of course, if the rule stated something like 

if is-a-man socrates and 

is-alive socrates 

then 

is-mortal socrates 

then asserting that is-a-man socrates would not be sufficient to complete 

the conditions of the rule. 

Most expert systems will consist of a large number of rules and require 

the assertion of a substantial number of facts to reach meaningful conclusions. Under P-BEST, when a fact is asserted and matched against all 

candidate rules, the resulting set of rules flagged as complete (all patterns 

in the antecedent are bound to some fact) are examined to determine if the 

there is a valid binding combination. This second level of analysis which 

deals with value constraints is called binding anafysi8. In general, variable values are examined and any additional test constraints are evaluated 
A.1. How P-BEST Works 51 

to determine if there is a consistent interpretation of the binding set that 

would allow a rule to reach its conclusion (or fire). The rules with rule/fact 

bindings that meet binding analysis are gathered into a conflict set, and 

the “best” rule in this set is selected and fired. The process of selecting a 

rule to fire from a number of possibilities is called conflict resolution. The 

consequent of the selected rule will fire and generally alter the state of the 

knowledge base, which will cause the creation of other rule/fact bindings. 

The process then repeats until no further candidates for firing remain. It 

is up to the individual application to assign an interpretation to this state: 

in some applications, exhausting all possible inferences might be considered 

the natural culmination of processing, while in other applications, reaching 

such a state might be considered an error. 

A.l.l Facts 

Facts in the P-BEST system may be thought of as predicates asserted into 

the fact base. At the lowest level, they are LISP structures whose format 

is described by a user-provided definition statement. A fact’s type is called 

its ptype (or puttern-type), and thus the function for defining fact types is 

called “define-ptype.” A sample ptype definition might be: 

(def ine-ptype is-mortal person) . 

This ptype, is-mortal, allows the assertion of facts into the system whose 

person field could contain something like socrates, or reagan or 6. It 

is necessary to note the difference between syntactic constraint, which the 

system enforces, and semantic constraint, which is the responsibility of the 

knowledge engineer. In the above example, is-mortal is a syntactic structure that takes a single argument: this is the extent of the restrictions 

enforced by the system. Semantically, the intent of this predicate is that 

the value occupying the person field is a mortal. Asserting, for instance, 

that (is-mortal air) or (is-mortal 6) is syntactically correct, but is of 

dubious semantic worth. 

Although facts are generally asserted into the knowledge base by rules, a 

user can directly alter the state of the knowledge base. The act of asserting a 

fact is handled by the function pbest-assert. The function pbest-assert 

allows the assertion of a single fact into the Fact Base. A fact assertion 

might look like this: 

(pbest-assert ’(is-mortal socrates)) 
52 Appendix A. P-BEST 

FB : [fl] 

1 

(&PZl) 

1 

(&PZ2) 

1 

nil 

C 

t 

U 

[%I =+ 

=+ [fnl 

1 

nil 

nil 

t 

IRZI 

U 

Figure A.l: Knowledge Base 

This would result in the assertion of a fact (or predicate) of type is-mortal, 

whose attribute is socrates. The fact would be added to the global knowledge base, and appropriate rules would examine the fact in an attempt to 

bind to it. 

A.1.2 Rule/Fact Bindings 

What does it mean for rules and facts to be bound? When a fact is asserted 

into the fact base, all rules pertaining to that fact (Le., which reference 

facts of a particular ptype) create links to it. These links are referred to as 

bindinge. Consider the symbolic examples of Figure A.l, which represents 

the state of the system after three rules (&, Ry, R,) have been added to the 

rule base, and three or more facts (fl, E, f3,. . .fn) have been asserted to the 

fact base. 

In this example, (where R=rule, P=pattern, and B=binding) rules & 

and 4 are candidates for binding analysis to determine if some combination 

of the current bindings constitutes a consistent binding context @e., all 

repeated variables have the same value, and all variable tests and restrictions 
A.2. P-BEST Components 53 

are satisfied). You will notice that R. is not a candidate for binding analysis 

because R.P.2 is not bound to any fact. Therefore, the COMPLETE flag 

(represented by the vertical “C”) is not set. R,, on the other hand, will be 

considered in binding analysis because 1R,,Pi,21 which is a not-pattern, has 

no bindings; all other patterns in R, have bindmgs. 

What does it mean for a binding context to be consistent? Briefly, PBEST checks each possible combination of the rule patterns and all matching 

facts until it finds a set of facts that are consistent. So, if a rule has two 

patterns, the first pattern having four facts that match it, and the second 

pattern having five facts that match it, then P-BEST may have to consider 

all possible pairs’. In this case, there are potentially 20 different comparisons 

to establish a consistent set of facts. 

A.2 P-BEST Components 

P-BEST consists of a production-rule language, a compiler, and a window 

debugger. These facilities are combined into an integrated environment for 

the creation and maintenance of knowledgebased systems. 

A.2.1 The Language 

The heart of any expert system shell is its facility for capturing knowledge. 

The P-BEST language is very expressive, allowing the knowledge engineer 

to capture complex relationships in a concise form, yet the syntax is constrained English, thereby greatly increasing the readability (and therefore, 

the maintainability) of P-BEST rules over other representations. 

A.2.2 The Compiler 

The implementation of P-BEST optimizes execution speed and avoids the 

use of an extensive run-time support package in favor of direct translation of 

the production rules into complete, independently compiled functions. Various run-time control logic and auxiliary functions are provided to support 

the execution of the rules, but the real heart of a P-BEST-based expert 

system is the generated functions that represent the rules themselves. 

It is perhaps misleading to say that P-BEST contains a compiler; it 

does not. P-BEST contains a translator that converts the rules from its 

‘P-BEsT’s optimized search strategy allows it to terminate its search upon finding the 

first consistent binding context 
54 Appendix A. P - BEST 

own representation language to CommonLisp functions. P-BEST then depends upon the operation of the target system’s CommonLisp compiler to 

complete the process of generating object code. This is all transparent to 

the knowledge engineer, however. 

Each production rule is translated into three main functions that implement the semantic intent of the rule: a function for examining newly 

asserted facts and creating proper rule/fact bindings; a function for analyzing binding relationships and determining consistency; and a function that 

implements the results, or consequent, of the rule. 

A.2.3 The Debugger 

The expert system development environment presented by P-BEST is greatly 

enhanced by the addition of a windowing debugger. Although this debugger 

is not intended to be used as part of a completed expert system, it is very 

useful during the creation and debugging of the rule base. 

The debugger provides multiple simultaneous views into the state of 

the knowledge base. In one window, the set of currently asserted facts is 

displayed along with binding information. In another window, the rules 

are displayed. The user is provided with numerous operations, such as 

commands to step through the execution of the rule base, commands to 

alter system state through assertion or negation of facts, and commands to 

activate tracing features. 
Appendix B 

Ehdrn 

The EHDM verification system was constructed at SRI International under 

the direction of Friedrich von Henke(1, 2, 3, 551. The following sections 

provide a brief overview of some of the features of the EHDM methodology. 

B.l The EHDM Specification Language and Logic 

This section provides a brief overview of the specification language of EHDM 

and the underlying logic. 

The specification language is based on first-order typed predicate calculus, but also includes elements of richer logics, such as higher-order logic [49], 

lambd&calculus [7] and Hoare logic [29], for greater expressiveness. For example, higher-order terms are particularly useful for expressing induction 

schemas and requirements. 

The specification language is strongly-typed; all entities must be declared 

with their type before use. The type system includes subtypes and function 

types. Specifications are written as definitions and formulas (axioms, theorems, and lemmas). In addition to the standard expressions, the language 

provides the Boolean connectives, polymorphic conditionals, and quantified 

expressions, including quantification over functions . A sublanguage is included for modeling operational behavior and imperative programs, based on the notions of state object and operation. State 

objects correspond to “program variables” in programming languages. Op 

erations express state transformations; they have an effect on state objects 

by possibly changing their values. 

55 
56 Appendix B. EHDM 

The sublanguage also includes constructs for composing operation expressions; these correspond to the common control structures of programming languages. The combination of all these features forms a sublanguage 

that is essentially equivalent to a simple subset of the Ada programming language. The semantics of operations are defined by Hoare formulas, which 

express properties of the states before and after the state transformation 

denoted by the operation. 

Specifications are organized around the concept of parameterized modules. Modules are closed scopes with explicit importation and exportation of 

names; modules can be nested. Names are made unique by qualifying them 

with the name of their module of origin. Modules may be parameterized 

by types, constants, and functions. Semantic assumptions or constraints on 

module parameters can be expressed; these entail an obligation that must 

be justified for each module instantiation. This form of module parameterization is very general and powerful; it supports generic specifications and 

allows many complex constructs to be built from simple language primitives. 

Modules are the basic building blocks of specifications. A module may rep 

resent the theory describing a specification concept, an abstract data type, 

an abstract state machine, or an (abstract) program. 

An important aspect of the EHDM language (and the EHDM approach 

in general) is the support of hierarchical development of specifications and 

proofs. The language supports hierarchical structuring of specifications, 

both with respect to composition of modules ( Uhorizontal hierarchy”) and 

levels of abstractions and refinements (“vertical hierarchy”). Vertical links 

between modules at adjoining abstraction levels are established by mappings, which generalize the notion of implementation. 

The language has been designed so that it naturally supports a high degree of reusability of specifications and proofs. Reusability is also enhanced 

by the library facility described later. 

B.2 The Theorem Prover of EHDM 

The theorem-prover component of EHDM combines powerful heuristics for 

mechanically generating proofs in first-order predicate logic with efficient 

decision procedures for the following standard theories: 

0 Ground formulas in propositional calculus 

0 Equality over uninterpreted function symbols [50] 
B.3. The EHDM Environment 57 

0 Presburger arithmetic, that is, linear arithmetic with the usual ordering relations [51] 

Quational reasoning similar to the use of rewrite rules is specially supported 

by the mechanized proof procedure. The prover also implements the main 

reduction rules of lambda calculus and a fragment of higher-order logic; 

however, the exact extent of this support is currently unclear. 

The system supports both automated proof generation and interactive 

proof construction that depends on user guidance. Proofs (more precisely, 

proof steps) are declared in the proof part of a specification module; they 

are expressed as a conclusion to be proven and a list of formulas (axioms 

and lemmas) from which the conclusion can be deduced. The automated 

prover completes a proof by attempting to construct suitable instances of 

the formulas involved; the user can help in this process by providing some 

substitutions for free variables, either directly in the proof declaration or 

during proof construction. Completed proofs can be captured in augmented 

proof declarations and included in the specification text for later %eplay.” 

A proof-chain analysis tool checks for completeness of larger proof trees and 

helps keep track of dependencies. 

A special procedure for reasoning about state transformations has builtin knowledge of the meaning of Hoare formulas and the constructs for expressing state objects and state transformations. This procedure provides 

the main support for code-level verification. It permits users to reason directly with Hoare formulas, without the traditional intermediate step of 

translating annotated programs into verification conditions (VCs); the procedure also supports reasoning about program fragments, as opposed to complete programs units (like subprograms). In these respects, the paradigm 

that is implemented by the procedure is more general than the traditional 

‘verification condition generator” (VCG) paradigm. However, the equivalent of a VCG is available in the EHDM environment as a proof development 

tool. 

B.3 The EHDM Environment 

The EHDM environment is implemented as an integrated, interactive system 

that supports all activities involved in creating, analyzing, modifying, managing, and documenting specification modules and proofs. The standard 

user interface of EHDM uses the bit-map display and combines a displayoriented text editor (customized and enhanced EMACS) with multiple win- 
58 Appendix B. EHDM 

dows, menus, and mouse input. (A less enhanced editor-based interface is 

available for remote operation.) All operations can be invoked directly from 

the editor, including the basic operations of parsing, prettyprinting, and 

typechecking specification text, invoking the theorem prover, and requesting 

status information. In addition to the basic operations just mentioned, the 

system provides a number of further support tools, including: the Context 

and Library tools, the configuration control support, and the MLS Checker 

and the EHDM-to-Ada translator (described in [3]). 

B.3.1 

The system maintains an internal data base for keeping track of the state 

of individual modules and proofs (referred to as the working contezt), and 

of the interdependences among modules and libraries; the user can manipulate this working context or switch between contexts. Modules are the 

basic entities around which the EHDM system is organized, and the context feature virtually insulates the user from the underlying file system; the 

EHDM system creates and manages ‘internal’ files, which the user can ignore 

completely because all file manipulation happens as a side effect of the user 

interaction with the EHDM system. 

The library mechanism permits users to group together standard modules in libraries of reusable concepts, theorems, and proofs. The environment offers tools for creating and maintaining module libraries and supports 

sharing of libraries among users and projects. 

Contexts and libraries have been designed so that the novice user can 

completely ignore these facilities. A user always works within a context, but 

when a user starts EHDM for the first time, the system automatically establishes a working context; later, when the user leaves EHDM the system saves 

the context and restores it when work is resumed. Users need to know about 

contexts only when they want to work in more than one context; similarly, 

they can ignore libraries until they want to make use of that facility. 

The Context and Library Manager 

B.3.2 The Configuration Control Tool 

A configuration and version control mechanism ensures that consistent versions of modules are used, and status checks report on the status of modules 

and proofs, and on dependencies among modules and proofs. At any given 

time, a module specification may be in one of several states. When a module is typechecked and also when a proof is performed, a “version check” is 
. 

B.3. The EHDM Environment 59 

made to see that the typecheck information recorded for the transitive closure of all referenced modules is still valid. For example, if module A uses 

module B, then changes to module B will invalidate the typecheck information recorded for module A. This will be discovered when the typecheck 

information for module A is used during the typechecking of a module that 

uses A, or during the construction of a proof from A or a module that uses 

A. 
Appendix C 

Tic-Tac-Toe Rule base 

;; Each position in the 3x3 board is represented in working 

;; memory by a “position” assertion of the following form: 

(define-ptype position row col marker) 

;; where rou,col are integers in the range 1-3 and marker is an 

;; element of the set free, opp, com. .. 

DS 

.. 

I. 

; ; A fact is asserted to keep track of whose turn it is .. 

*I 

(define-ptype turn player count) 

;; where player is an element of the set opp, com, and count is 

; ; of type nat. .. 

OD 

;; The initial state consists of 9 position assertions and 1 turn 

;; assertion. 

.. 

DD 

;; A fact is asserted as the result of a player move, prior to 

;; altering the board position. so that it may be checked. 

61 
62 Appendix C. Tic-Tac-Toe Rule base 

(def ine-ptype oppmove row col) 

.. 

BO 

.. 

#I 

.. 

*B 

.. 

BI 

.. 

OB 

.. 

## 

where row and column are integers in the range of 1-3 which 

must correspond to a free position on the board. 

The following macros are defined for convenience: 

(defmacro cornerp (x y) ‘(and (oddp .x)(oddp By))) 

(defmacro middlep (x y) ‘(or (and (oddp ,x)(evenp ,y)) 

(defmacro centerp (x y) ‘(and (equal ,x 2)(equal ,y 2))) 

(and (evenp ,x)(oddp ,y>))) 

.. 

1) 

.. 

BI 

(defrule blk-cc states 

if there exists a turn called ti 

such that player is com and 

count is 3 and 

such that row is ?rl and 

col is ?cl and 

marker is opp and 

there exists a position 

there exists a position 

such that row is ?r2 and 

col is ?c2 and 

marker is opp 

with (and (not (equal ?rl ?r2)) 

(not (equal ?cl ?c2)) 

(cornerp ?rl ?cl) 

(cornerp ?r2 ?c2) 

there exists a position 

such that row is 2 and 

col is 2 and 

marker is com and 
63 

there exists a position called pl 

such that row is ?r3 and 

col is ?c3 and 

marker is free 

with (middlep ?r3 ?c3) 

then forget tl and 

forget pl and 

remember a position 

which inherits from pi 

except that marker is com and 

remember a turn 

such that player is opp and 

count is 4) 

(defrule blk-cm states 

if there exists a turn called ti 

such that player is com and 

count is 3 and 

such that row is ?rl and 

col is ?cl and 

marker is opp and 

there exists a position 

there exists a position 

such that row is ?r2 and 

col is ?c2 and 

marker is opp 

with (and (not (equal ?rl ?r2)) 

(not (equal ?cl ?c2)) 

(cornerp ?rl ?cl) 

(middlep ?r2 ?c2)) 

there exists a position 

such that row is 2 and 

col is 2 and 

marker is com and 

there exists a position called pi 
64 Appendix C. Tic-%-Toe Rule birse 

such that row is ?r3 and 

col is ?c3 and 

marker is free 

with (and (and (oddp ?r3) ;; take corner which intersects 

(oddp ?c3)) ;; both of opp’s markers 

(or (and (equal ?r3 ?rl) 

(and (equal ?r3 ?r2) 

(equal ?c3 ?c2) 1 

(equal ?c3 ?ci)))) 

then forget ti and 

forget pl and 

remember a position 

which inherits from pl 

except that marker is com and 

remember a turn 

such that player is opp and 

count is 4) 

(defrule win-col at rank 1 states 

if there exists a turn called tl 

such that player is com and 

such that row is ?rl and 

col is ?cl and 

marker is com 

there exists a position 

there exists a position 

such that row is ?r2 and 

col is ?c2 and 

marker is com 

(equal ?cl ?c2)) and 

with (and (not (equal ?rl ?r2)) 

there exists a position called pos 

such that col is ?c3 and 

marker is free 

with (equal ?c2 ?c3) 
65 

then 

forget ti and 

forget pos and 

remember a position 

which inherits from pos 

except that marker is com) 

(defrule winrow at rank 1 states 

if there exists a turn called ti 

such that player is com and 

such that row is ?rl and 

col is ?cl and 

marker is com 

there exists a position 

there exists a position 

such that row is ?r2 and 

col is ?c2 and 

marker is com 

(not (equal ?cl ?c2))) and 

with (and (equal ?rl ?r2) 

there exists a position called pos 

such that row is ?r3 and 

marker is free 

with (equal ?r2 ?r3) 

forget pos and 

forget ti and 

remember a position 

then 

which inherits from pos 

except that marker is com) 
66 Appendix C. Tic-Tac-Toe Rule base 

(defrnle winAia at rank 1 states 

if there exists a turn called tl 

such that player is corn and 

such that row is ?rl and 

col is ?cl and 

marker is corn 

there exists a position 

there exists a position 

such that row is ?r2 and 

col is ?c2 and 

marker is corn 

with (and (not (equal ?rl ?r2)) 

(not (equal ?cl ?c2)) 

(equal (ab8 (- ?rl ?r2)) 

(ab8 (- ?cl ?c2)))) and 

there exists a position called pos 

such that row is ?r3 and 

col is ?c3 and 

marker is free 

with (and (equal (abs (- ?rl ?r3)) 

(equal (abs (- ?r2 ?r3)) 

(abs (- ?cl ?c3))) 

(abs (- ?c2 ?c3)))) 

then 

forget pos and 

forget tl and 

remember a position 

which inherits from pos 

except that marker is corn) 

(defrule blk-col states 

if there exists a turn called tl 

such that player is corn and 

count is ?x and 

there exists a position 
67 

such that row is ?rl and 

col is ?cl and 

marker is opp 

there exists a position 

such that row is ?r2 and 

col is ?c2 and 

marker is opp 

(equal ?cl ?c2)) and 

with (and (not (equal ?rl ?r2)) 

there exists a position called pos 

such that col is ?c3 and 

marker is free 

with (equal ?c2 ?c3) 

forget pos and 

forget tl and 

remember a position 

then 

which inherits from pos 

except that marker is corn and 

remember a turn 

such that player is opp and 

count equals (1+ ?XI) 

(defrnle blkrow states 

if there exists a tarn called tl 

such that player is corn and 

count is ?x and 

there exists a position 

such that row is ?rl and 

col is ?cl and 

marker is opp 

there exists a position 

such that row is ?r2 and 

col is ?c2 and 

marker is opp 
68 Appendix C. Tic-Tac-Toe Rule base 

with (and (equal ?rl ?r2) 

(not (equal ?cl ?c2))) and 

there exists a position called pos 

such that row is ?r3 and 

marker is free 

with (equal ?r2 ?r3) 

forget pos and 

forget ti and 

remember a position 

then 

which inherits from pos 

except that marker is com and 

remember a turn 

such that player is opp and 

count equals (l+ ?XI> 

(defrule blk-dia states 

if there exists a turn called ti 

such that player is com and 

count is ?x and 

there exists a position 

such that row is ?rl and 

col is ?cl and 

marker is opp 

there exists a position 

such that row is ?r2 and 

col is ?c2 and 

marker is opp 

with (and (not (equal ?rl ?r2)) 

(not (equal ?cl ?c2)) 

(equal (abs (- ?rl ?r2)) 

(abs (- ?cl ?c2)))) and 

there exists a position called pos 

such that row is ?r3 and 

col is ?c3 and 
69 

marker is free 

with (and (equal (abs (- ?rl ?r3)) 

(equal (abs (- ?r2 ?r3)) 

(abs (- ?cl ?c3))) 

(abs (- ?c2 ?c3)))) 

then 

forget pos and 

forget tl and 

remember a position 

which inherits from pos 

except that marker is com and 

remember a turn 

such that player is opp and 

count equals (1+ ?XI) 

(defrule see-wongame at rank 2 states 

if there exists a turn called tl and 

such that row is ?rl and 

col is ?cl and 

marker is ?m 

there exists a position 

with (not (equal ?m 'free)) and 

there exists a position 

such that row is ?r2 and 

col is ?c2 and 

marker is ?m 

with (or (not (equal ?r2 ?rill 

(not (equal ?c2 ?cl))) and 

there exists a position 

such that row is ?r3 and 

col is ?c3 and 

marker is ?m and 

with (and (or (not (equal ?r3 ?r2)) 

(or (not (equal ?r3 ?rl)) 

(not (equal ?c3 ?c2) 1) 
70 Appendix C. Tic-Tu-Toe Rule base 

(not (equal ?c3 ?cl)))> and 

test (or (and (equal ?rl ?r2) 

(and (equal ?cl ?c2) 

(and (equal (ab8 (- ?rl ?r3)) 

(equal (abs (- ?r2 ?r3)) 

(not (or (equal ?rl ?r2) 

(equal ?rl ?r3)) 

(equal ?cl ?c3)) 

(abs (- ?cl ?c3))) 

(abs (- ?c2 ?c3))) 

(equal ?cl ?c2) 1) 1) 

then forget ti and 

execute (draw-board) and 

execute (format t "'%Player -A Won The Game! ! !'%" ?m)) 

(defrule see-tiegame at rank 2 states 

if there exists a turn called ti 

such that player is ?p and 

there does not exist a position 

such that marker is free 

then forget tl and 

execute (format t "%Tie Game! ! !'%")) 

(defrule makerandomaove at rank -10 states 

such that player is com and 

there exists a position called pl 

if there exists a turn called tl 

count is ?x and 

such that marker is free 

then forget pi and 

forget ti and 
71 

remember a position 

which inherits from pi 

except that marker is com and 

remember a turn 

such that player is opp and 

count equals (I+ ?XI) 

(def rule getappaove states 

if there exists a turn 

such that player is opp and 

there exists a position 

such that marker is free and 

there does not exist an oppaove 

then execute (draw-board) and 

remember an oppaove 

such that row equals (get-ans 'row) and 

such that col equals (get-ans 'col)) 

(def rule do-oppaove states 

if there exists a turn called tl 

such that player is opp and 

there exists an oppiove called mi 

count is ?x and 

such that row is ?rl and 

col is ?cl and 

such that row is ?rl and 

col is ?cl and 

marker is free 

there exists a position called pl 

then forget ti and 

forget ml and 
72 Appendix C. Tic-Tac-Toe Rule base 

forget pi and 

remember a position 

which inherits from pl 

except that marker is opp and 

remember a turn 

such that player is com and 

count equals (1+ ?XI) 

(def rule bad-opp-move states 

if there exists a turn 

such that player is opp and 

there exists an opp-move called ml 

such that row is ?rl and 

col is ?cl and 

such that row is ?rl and 

col is ?cl and 

marker is ?m with (not (equal ?m 'free)) 

there exists a position 

then forget ml and 

execute (format t "'%That position is already taken! 'X1I)) 

(defun init-ttt (1 

(Prow 

(pest -reset ) 

(pest-assert ' (position 3 2 free)) 

(pest-assert '(position 2 3 free)) 

(pest -assert ' (position 2 1 f reel ) 

(pest-assert I (position 1 2 free)) 

(pest-assert ' (position 3 3 free)) 

(pest-assert I (position 3 1 free)) 

(pest-assert '(position 1 3 free)) 
73 

(pest-assert '(position 1 1 free)) 

(pest-assert ' (position 2 2 free) 1 

(pest-assert ' (turn opp 0)) 1) 

(defun get-ans (label) 

(do ((x 0)) 

((and 

(format t "'%Enter 'A (1-3): 'I label) 

(setf x (read)))) 

(> x O)(< x 4)) x) 

(defun draw-board () 

(format t n'%r 

c: 1 : 2 : 3 '%"I 

(do ((r l)(c 1 (1+ c))) 

((and (= r 3)(> c 3))) 

(if (> c 3) 

(prop (setf c 1) 

(incf r) 

(format t "'X ---+---+--- 'X"))) 

(if (3 c 1) (format t 'A :n r)) 

(format t " 'A 

(if (< c 3) (format t 111")>)) 

(print-marker r c)) 

(defun print-marker (row col) 

(dolist (f *facts*) 

(if (and (position-p (f act-body (eval f) 

(equal (position-row (fact-body (eval f )) row) 
74 Appendix C. Tic-Tac-Toe Rule base 

(equal (position-col (fact-body (eval f))) col)) 

(if (equal (position-marker (f act-body (eval f 1)) 'opp) 

(return ' 0) 

(if (equal (position-marker (fact-body (eval f ))I 'corn) 

(return 'XI 

(return #\Space)))))) 
Appendix D 

Tic-Tac-Toe Specifications 

75 
76 Appendix D. Tic- Tac- Toe Specifications 

arrays: Module [dtype: TYPE, undef-r: dtype] 

Exporting array, newarray, assign, *1[*1], length, dtype 

Theory 

array: TYPE 

i, j: VAR nat 

d VARdtype 

a: VAR array 

newarray: array 

assign: function[array, nat, dtype -+ array] 

*1[*1]: function[array, nat + dtype] 

length: function[array -+ nat] 

acessnew: Axiom newarray[;] = undefi. 

selectassign: Axiom a := i[j] = if i = j then d else a[j] end if 

undax: Axiom (i 5 0 V i > length(a)) 2 a[;] = undef-r 

End arrays 
77 

data: Module 

Exporting datum, undef, wild 

Theory 

datum: TYPE IS int 

undef, wild: datum 

daxl: Axiom undef # wild 

End data 
78 Appendix D. Tic-Tac-Toe Specifications 

diffs: Module 

Exporting I * - * I, oddp, evenp 

Theory 

n,m: VAR nat 

I * - * I: function(nat, nat + nat] 

oddp: function[int + bool] 

evenp: function[int + bool] 

diffax: Axiom I n - rn I= if n > rn then n-rn else m-n end if 

oddp-ax: Axiom 

oddp(n) = if n = 1 

then true 

ELSIFn > 1 then oddp(n - 2) else false 

end if 

evenp-ax: Mom 

evenp(n)= if n=O 

then true 

ELSIF'n > 1 then evenp(n - 2) else false 

end if 

natdef-ax: Axiom n 2 0 

Proof 

difflemma: Lemma I n - m 12 0 

dlp: Prove difflemma from 

diffax {n t nQcs, m t mQcs}, 

natdefax {n t nQCS}, 

natdef-ax {n t mQcs} 

End diffs 
79 

facts: Module 

Using data, arrays[datum, undef] 

Exporting fact with data, arraya[datum, undef] 

Theory 

fact: TYPE from array 

End facts 
80 Appendix D. Tic-Tac- Toe Specifications 

sets: Module [t: TYPE] 

Exporting set, 0, UNIVERSE, {*l}, E, C, C, n,U, \,a, 

setdesseq, sets.less, sets.times, seta.plus, sets.difference, 

setsminus, seteq 

Theory 

set: TYPE 

0: set 

UNIVERSE: set 

S1, S2, S3: VAR set 

z,y: VAR t 

{*I}: function[t -+ set] 

E: function[t, set 4 bool] 

C: function[set, set 4 bool] 

c: function[set, set + bool] 

n: function[set, set + set] 

U: function[set, set -+ set] 

\: function[set, set -+ set] 

*I: function[set --r set] 

seteq: function[set, set -+ bool] 

SETdef: Axiom (z E {z}) A ((y E {z}) 

subdef: Axiom (S1 C S2) 

psubdef: Axiom 

interdef: Axiom (z E (S1 n S2)) u ((2 E S1) A (z E S2)) 

uniondef: Axiom (z E (S1 U S2)) e, ((2 E Sl) V (z E S2)) 

diffdef: Axiom (z E (S1\ S2)) e, ((2 E S1) A ~(z E S2)) 

compdef: Axiom (z E n) e, (~(z E Sl)) 

eqdef: Axiom Sl = S2 * seteq(S1, S2) 

eqx Formula seteq(S1, S1) 

eqs: Formula seteq(S1, S2) e seteq(S2, Sl) 

eq-t: Formula (seteq(S1, S2) A seteq(S2, S3)) 3 seteq(S1, S3) 

- 

z = y) 

(V x: (z E S1) 3 (z E S2)) 

(SI C s2) (((2 E SI) 3 (2 E s2)) A (3~: (y E s2) A l(y E SI))) 
81 

sb-t: Formula ((Sl C S2) A (S2 C S3)) 2 (S1 C S3) 

seteqdef: Axiom 

nulldef: Axiom (z E 0) = false 

nulldef2: Axiom (Vx: l(z E Sl)) e, S1 = 0 

unidef: Axiom (z E UNIVERSE) = true 

sub-reflex: Formula (S1 5 S1) = true 

interidentity: Formula S1 = (S1 n S1) 

inter-commutative: Formula (S1 n S2) = (S2 n S1) 

internull: Formula (S1 n 0) = 0 

interassoc: Formula (S1 n (S2 n S3)) = ((Sl n S2) n S3) 

union-commutative: Formula (S1 u S2) = (S2 u S1) 

union-associative: Formula (S1 U (S2 U S3)) = ((Sl U S2) U S3) 

unionidentity: Formula (S1 U S1) = S1 

unionnull: Formula (S1 U 0) = S1 

doubleneg: Formula = S1 

negnull: Formula 5 = UNIVERSE 

neg-uni: Formula UNIVERSE = 0 

uni-union: Formula (S1 u E) = UNIVERSE 

nullinter: Formula (S1 n sl> = 0 

diffinter: Formula (S1\ S2) = (S1 n E) 

End sets 

seteq(S1,SZ) tj (vx: ((z E SI) 3 (z E S2)) A ((z E S2) 3 (z E SI))) 
82 Appendix D. Tic- Tac-Toe Specifications 

states: Module 

Exporting state, SO, next 

Theory 

state: TYPE IS nat 

SO: state = 0 

SI, 92: VAR state 

next: function[state + state] = ( X s1 -+ state : (91 + 1)) 

nonneg: Axiom s1 2 SO 

succ: Axiom s1 > SO 3 (3 82 : next(s2) = SI) 

End states 
83 

ttt-ptypes: Module 

Using facts, states, kbs, sets[fact], diEs 

Exporting row, col, marker, player, count, turn, oppmove, 

position, turnp, oppmove-p, positionp, tttptypes.equals, opp, com, 

free, match-turn, matchappmove, matchposition, akb, cornerp, 

middlep, centerp 

Theory 

row: nat = 1 

col: nat = 2 

marker: nat = 3 

player: nat = 1 

count: nat = 2 

opp, com, free: datum 

turn, oppmove, position: TYPE from fact 

f: VAR fact 

t,tl: VAR turn 

0: VAR oppmove 

dl, d2, d3: VAR datum 

rx, cx, IN[, px: VAR datum 

kbx: VAR kb 

sx: VAR state 

akb: kb 

turn-p: function[fact + bool] 

match-turn: function[kb, state, fact, datum, datum + bool] = 

P, P1, P2, Ps, P4, P5, P6, P7, P8, P9: VAR position 

(A kbx, sx, f, dl, d2+ bool : 

(f E kbinst(kbx, sx)) 

A t--P(f 1 

A (dl = wild V dl = f[player]) A (d2 = wild V d2 = f[count])) 

oppmove-p: function[fact + bool] 

match-oppmove: function[kb, state, fact, datum, datum + bool] = 

(A kbx, sx, f, dl, d2+ bool : 

(f E kbinst(kbx, sx)) 

A oppmove44f) 

A (dl = wild V dl = f[row]) A (d2 = wild V d2 = f[col])) 
a4 Appendix D. Tic- Tac- Toe Specifications 

positionp: function[fact + bool] 

matchqosition: function[kb, state, fact, datum, datum, datum + bool] 

= (A kbx, sx, f, dl, d2, d3+ bool : 

(f E kbinst(kbx, sx)) 

A poaitionp( f) 

A (dl = wild V dl = f[row]) 

A (d2 = wild V d2 = f[col]) A (d3 = wild V d3 = f[marker])) 

equals: function[position, position + bool] = 

(Apl ,p2+b00l: 

PI [row] = PZ [row] 

A pi [col] = pz [col] A p1 [marker] = p2 [marker]) 

cornerp: function[fact -, bool] = 

centerp: function[fact + bool] = 

middlep: function[fact + bool] = 

(A f+ bool : position+(f) A oddp(f[row]) A oddp(f[col])) 

(A f+ bool : position+(f) A f[row] = 2 A f[col] = 2) 

(Af+ bool : 

position+( f) 

A ((....P(f[row]) A oddP(f[coll)) 

v (oddP(f[rowl) A evenP(f[coll)))) 

distinctxonstants: Axiom 

opp # corn A com # free 

A opp # free A opp # wild A com # wild A free # wild 

trnlthax: Axiom length(t) = 2 

opplthax: Axiom length(o) = 2 

poslthax: Axiom length(p) = 3 

fact-type-1: Axiom turn-p(f) v oppmovep(f) v position&) 

fact-type2: Axiom turnp(f) 3 -(oppmovep(f) v position+(f)) 

fact-type-3: Axiom oppmove-p(f) 3 -(turn-p( f) v position+( f)) 

fact-type-4: Axiom positionp( f) 3 -(oppmove-p(f) v turnp( f)) 
85 

fact-type-5: Axiom tump(t) A l(tum_p(o) v tum-p(p)) 

fact-types: Axiom oppmove-p(o) A -(oppmovep(t) V oppmove-p(p)) 

fact-type-7: Axiom position&) A -.l(position-p(t) v positionp(0)) 

possible-positions: Axiom 

(p E kbinst(akb, sx)) 

Ap[row] 5 3 

* (p[row] 2 1 

Ap[col] 2 1 

Ap[col] 5 3 

A marker] = free V marker] = opp V marker] = 

corn)) 

duplicate-positions: Axiom 

((p E kbinst(akb, sx)) 

A (p1 E kbinst(akb, sx)) A p[row] = pl[row] A p[col] = pl[col]) 

3 marker] = pl[marker] 

possible-turns: Axiom 

(t E kbinst(akb, sx)) 

tj ((t[player] = com V t[player] = opp) A p[count] 1 0) 

End tttptypes 
86 Appendix D. Tic-Tac-Toe Specifications 

tttilal: Module 

Using tttptypes, states, facts, kbs, sets[fact] 

Exporting makemove, makemovelhs 

Theory 

f: VAR fact 

r,c: VAR nat 

tl, t2: VAR turn 

s1,s2: VAR state 

makemove: function[kb, state + state] 

makemovelhs: function[kb, state -+ bool] 

makemovedef: Axiom 

Pl, P2, Ps, P4, P5, P6, P7, P8, P9, Po: VAR position 

(3tl , P1 : 

if matchfurn(akb, SI, tl, corn, wild) 

A matchposition( akb, 81, p1, wild, wild, free) 

then makemove(akb, SI) = next(s1) 

A -(tl E kbinst(akb, next(s1))) 

A -.1(p1 E kbinst(akb, next(s1))) 

A(3t2: 

match-turn(akb, next(sl), t2, opp, wild) 

A t2[count] = 1 + tl[count]) 

WP2: 

match-position(akb, next(sl), pz, wild, wild, corn) 

A P2 [row] = P1 [row] A P2 [col] = Pl[COl]) 

else makemove(akb, 91) = SI 

endif ) 

makemovelhsdef Axiom 

makemovelhs(akb, SI) 

*(3tl,P1: 

match-turn(akb, SI, tl, corn, wild) 

A matchposition(akb, 91, p1, wild, wild, free)) 

movenrder-1: Axiom 

makemove(akb, SI) = next (51) 
a7 

 PI ,PZ: 

(matchposition(akb, s1,p1,2,2, free) 

3 match-position(akb, next(sl),pz, 2,2, corn))) 

movesrder2: Axiom 

makemove(akb, 81) = next(s1) * (3Pl ,P2 ,Ps: 

((lmatchposition(akb, sl,p1,2,2,fiee) 

A matchposition(akb, sl,p2,1,l,fiee)) 

3 matchposition(akb, next(sl), ps, 1,1, corn))) 

move-orderf : Axiom 

makemove(akb, 81) = next(s1) * (3Pl ,P2 2Ps ,p4: 

((lmatchposition(akb, sl,p1,2,2,free) 

A -match-position(akb, s1,p2,1,1, free) 

3 matchposition(akb, next(sl),pd,l, 3, corn))) 

A match-position(akb, SI, ps, 1,3, free)) 

move-order-4: Axiom 

makemove(akb, SI) = next(s1) * (3P1 ,P2 9P3 9P4, P5: 

((-matchposition(akb, 81, p1,2,2, free) 

A lmatchposition(akb, sl,p2,1,1,free) 

A lmatch-position(akb, SI, ps, 1,3, free) 

A match-position(akb, 81, p4,3,1, free)) 

3 matchposition(akb, next(sl), p5,3,1, corn))) 

movenrder-5: Axiom 

makemove(akb, 81) = next(s1) * (3Pl ,P2 ,Ps ,P4 ,P5,P6: 

((-matchposition(akb, sl,p1,2,2,free) 

A lmatchposition(akb, sl,p2,1,1,free) 

A lmatchposition(akb, 81, ps, 1,3, free) 

A lmatchposition(akb, ~1,p4,3,1, free) 

A matchposition(akb, 81, p5,3,3, free)) 

3 matchposition(akb, next(sl), p6,3,3, corn))) 
88 Appendix D. Tic-Tac-Toe Specifications 

move~rder-6: Axiom 

makemove(akb, SI) = next(s1) 

*((3Pl,pZ,Ps,P4,P5,P6,P7: 

((-match-position(akb, sI,p1,2,2,free) 

A ymatchposition(akb, sl,p2,1,1, free) 

A lmatch-position(akb, sl,ps,l, 3, free) 

A -matchposition(akb, 81, p4,3,1, free) 

A -match-position(akb, SI, p5,3,3, free) 

A matchposition(akb, SI, p6,1,2, free)) 

1 match-position(akb, next(sl), p7,1,2, corn))) 

move-order-7: Axiom 

makemove(akb, 91) = next(s1) 

* @PI 2 P2 9 PS , P4 , P5, P6, P7, P8: 

((-match-position(akb, s1,pl, 2,2,free) 

A -matchposition(akb, s1,pz, 1, 1, free) 

A -.matchposition(akb, sl,pS,l, 3,free) 

A imatchposition(akb, 81, p4,3,1, free) 

A lmatchposition(akb, 81, p5,3,3, free) 

A -matchposition(akb, 91, p6,1,2, free) 

Amatch-position(akb, 81, p7,2,1, free)) 

1 matchposition(akb, next(sl), p8,2,1, corn))) 

move-orders: Axiom 

makemove(akb, SI) = next(s1) 

* (3Pl , P2 > PS , P4 , P5, P6, P7, P8, P9: 

((lmatch_position(akb, s1,p1,2,2, free) 8 A lmatchposition(akb, 81,p2,1,1,free) 

A lmatchposition(akb, sl,pS,l, 3, free) 

A lmatchposition(akb, SI, p4,3,1, free) 

A lmatchposition(akb, 91, p5,3,3, free) 

A lmatchposition(akb, 81, p6,1,2, free) 

Almatch-position(akb, 91, p7,2, I, free) 

Amatchposition(akb, SI, p8,2,3, free)) 
89 

3 match-position(akb, next(sl), p9,2,3, corn))) 

move-order-9: Axiom 

makemove(akb, SI) = next(s1) * (3Pl 9 P2 9 Ps 9 P4 , P5, P6, P7, P8, P9, Po: 

((lmatchposition(akb, sl,p1,2,2, free) 

A lmatchposition(akb, sl,p2,1,1, free) 

A -matchposition(akb, 81, ps, 1,3, free) 

A lmatchposition(akb, ~1,~4,3,1, free) 

A -.matchposition(akb, SI, p5,3,3, free) 

A -match-position(akb, SI, p6,1,2, free) 

Almatch-position(akb, SI, p7,2,1, free) 

A-match-position(akb, SI, p8,2,3, free) 

Amatchposition(akb, 81, p9,3,2, free)) 

3 matchposition(akb, next(sl), PO, 3,2, corn))) 

End tttllsl 
90 Appendix D. Tic- Tac- Toe Specifications 

ttt-rls2: Module 

Using tttptypes, states, facts, kbs, sets[fact] 

Exporting win-col, win-row, windia, winxol-lhs, winiowlhs, 

windialhs 

Theory 

f: VAR fact 

t, tl, t2: VAR turn 

p,cl, c2,pl,p2,ps,p4: VAR position 

SI, s2: VAR state 

win-col: function[kb, state + state] 

winlow: function[kb, state + state] 

windia: function[kb, state state] 

win-collhs: function[kb, state + bool] 

winiowlhs: function[kb, state + bool] 

win-dialhs: function[kb, state 4 bool] 

win-col-def: Axiom 

(-1 ,P1 ,P2 ,ps: 

if match-turn(akb, SI, tl, com, wild) 

A match-position(akb, 91, p1, wild, wild, com) 

A matchposition( akb, SI, pz, wild, wild, com) 

A matchposition(akb, SI, ps, wild, wild, free) 

A Pl[COl] = P2 [col] 

A P1 [row] # P2 [row] 

A PS[COl] = P2 [toll 

A Ps [row] # P1 [row] A PS [row] # P2 [row] 

then (3p4 : 

win-col(akb, SI) = next(s1) 

A l(t1 E kbinst(akb,next(sl))) . A -(ps E kbinst(akb, next(s1))) 

A matchposition(akb, next(sl), p4, wild, wild, corn) 

A Pr[rowI = Ps[rowl 

A p4 [col] = PS [col] 

P f PS 

A (vp: 

3 ((p E kbinst(akb, 81)) 

e> (p E kbinst(akb,next(sl)))))) 
91 

else win-col(akb, SI) = 81 

end if ) 

win-rowdef: Axiom 

(3tl , P1 , P2 , Ps: 

if match-turn(akb, 81, tl, com, wild) 

A matchposition(akb, 81, p1, wild, wild, com) 

A match-position(akb, SI, p2, wild, wild, corn) 

A matchposition(akb, SI, ps, wild, wild, free) 

A Pl[COlI # P2 [col] 

A p1 [row] = pz [row] 

A Pz[row] = Ps[row] 

A Ps [toll # Pl[COlI A P3 [4 # P2 [toll 

then (3p4 : 

winiow(akb, SI) = next(s1) 

A l(t1 E kbinst(akb, next(s1))) 

A l(p3 E kbinst(akb, next(s1))) 

A matchposition(akb, next(sl), p4, wild, wild, com) 

A ~4 [row] = PS [row] 

A P4 [c04 = Ps [col] 

P # Ps 

A(vp: 

3 ((p E kbinst(akb, 81)) 

(p E kbinst(akb, next(s1)))))) 

else win_row(akb, SI) = SI 

end if ) 

win-diadef: Axiom 

(3ti ,Pi ,P2 ,Ps: 

if match-turn(akb, SI, tl, corn, wild) 

A matchposition(akb, 81, p1, wild, wild, com) 

A match-position(akb, SI, pa, wild, wild, corn) 

A matchposition(akb, s1,ps, wild, wild, free) 

A P1 [row] # P2 [row] 

A Pl[COl] # P2[COl] 

A P1 [row] # Ps [row] 

A Pl[COl] # PS[COl] 

A P2[roWl # PS[rowl 
92 Appendix D. Tic- Tac- Toe Specifications 

A P2 [toll # Ps [col] 

A ((cornerp(p1) 

A centerp(pz) A centerp(p3)) 

v (centerp(p1) 

A cornerp(pz) A cornerp(ps))) 

then (3p4 : 

windia(akb, 81) = next(s1) 

A l(t1 E kbinst(akb, next(s1))) 

A ~(ps E kbinst(akb, next(s1))) 

A match-position(akb, next(sl), p4, wild, wild, com) 

A ~4[row] = ps[row] 

A P4 [coll = Ps [col] 

PfPs 

A(vp: 

3 ((p E kbinst(akb, 81)) 

e+ (p E kbinst(akb, next(s1)))))) 

else windia(akb, 81) = s1 

endif ) 

win-collhsdef: Axiom 

win-collhs(akb, 81) 

*(% ,P1 YP2 YPS: 

matchfurn(akb, 81, tl, com, wild) 

A match-position(akb, SI, p1, wild, wild, com) 

A match-position(akb, 51, pz, wild, wild, com) 

A P1 [col] = Pz [col] 

A P1 [row] # P2 [row] 

A match-position(akb, s1,ps, wild, wild, free) 

A PS[COl] = P2[C09) 

winiowlhsdefi Axiom 

winiowlhs(akb, SI) 

*(%,P1,Pz,Ps: 

match-turn(akb, 81, tl, corn, wild) 

A match-position(akb, s1,p1, wild, wild, com) 

A matchposition(akb, 81,p2, wild, wild, corn) 

A matchposition(akb, 81, ps, wild, wild, free) 

A P1 [toll # P2 [col] 
93 

win-dialhs-def: Axiom 

windialhs(akb, 81) * (3tl , P1 , P2 , Ps : 

match-turn(akb, 81, tl, com, wild) 

A rnatchposition(akb, s1,p1, wild, wild, corn) 

A matchposition(akb, 81, p2, wild, wild, corn) 

A matchposition(akb, 81, ps, wild, wild, free) 

A P1 [row] # P2 [row] 

A P1 [col] # P2 [toll 

A P1 [row] # Ps [row] 

A PI [col] # PS [col] 

A ~2 [row] # PS [row] 

A ~2 (~011 # PS[CO~] 

A ((cornerp(p1) 

A centerp(p2) A centerp(p3)) 

v (centerp(p1) 

A cornerp(p2) A cornerp(p3)))) 

End ttt-rls2 

-&. C- 
94 Appendix D. Tic-Tac-Toe Specifications 

tttils3: Module 

Using tttptypes, states, facts, kbs, sets[fact], diffs 

Exporting blk sol, blk ow , blk dia, blk xollhs , blk low lhs , 

Theory 

f: VAR fact 

tl, t2: VAR turn 

cl,c2,pl,p2,ps,p4: VAR position 

SI, 82: VAR state 

blk-col: function[kb, state -+ state] 

blkiow: function[kb, state --* state] 

blkdia: function[kb, state -+ state] 

blkxollhs: function[kb, state ---t bool] 

blkJowlhs: function[kb, state -+ bool] 

blkdialhs: function[kb, state ---t bool] 

blk-col-def: Axiom 

blkdialhs 

(-1 , P1 , P2 9 Ps : 

if match-turn(akb, SI, tl, com, wild) 

A matchposition(akb, SI, p1, wild, wild, opp) 

A matchposition(akb, SI, p2, wild, wild, opp) 

A P1 [col] = P2[4 

A P1 [row1 # P2 [row1 

A matchposition(akb, SI, ps, wild, wild, free) 

A P2 [col] = Ps [co4 

then (3p4 , t2: 

blk-col(akb, SI) = next(B1) 

A l(t1 E kbinst(akb, next(s1))) 1 A l(ps E kbinst(akb, next(s1))) 

Amatchposition(akb, next(sl), p4, ps(row], ps[col], com) 

A match-turn(akb, next(sl), t2, opp, wild) 

A t2[count] = 1 + tl [count]) 

else blk-col(akb, SI) = SI 

endif ) 

blkiowdef: Axiom 

(3tl ,Pl ,P2 ,ps: 
95 

if matchfurn(akb, SI, tl, com, wild) 

A match-position(akb, s1,p1, wild, wild, opp) 

h matchposition(akb, s1,p2, wild, wild, opp) 

A p1 [row] = pz [row] 

A Pl[COl] # P2 [toll 

A matchposition(akb, 81, ps, wild, wild, free) 

A P2 [row] = Ps [row] 

then (3p4 , t2: 

blk-row(akb, SI) = next(s1) 

A l(t1 E kbinst(akb, next(s1))) 

A -(ps E kbinst(akb,next(sl))) 

Amatch-position(akb, next(sl),p4,ps[row],ps[col], com) 

A match-turn(akb, next(sl), t2, opp, wild) 

A t2[count] = 1 + tl[count]) 

else blkJow(akb, 81) = s1 

end if ) 

blk-diadefi Axiom 

(3tl,Pl,n,Ps: 

if match-turn(akb, 81, tl, com, wild) 

A match-position(akb, s1,p1, wild, wild, opp) 

A matchposition(akb, SI, p2, wild, wild, opp) 

A matchposition(akb, 91, ps, wild, wild, free) 

A P1 [row] # P2 [row] 

A Pl[CO~] # P2[COl] 

A I Pl[rowl - Pz[roWl I=[ Pl[COl] - PZ[COl] I 

A I Pl[row] - Ps[row] I=I Pl[COl] - Ps[COl] I 

A I ~2[rowI - PS[~OW] I=I P~[CO~] - PS[CO~] I 

then (3p4 , t2: 

blkdia(akb, 81) = next(s1) 

A l(t1 E kbinst(akb, 82)) 

A -(ps E kbinst(akb, 82)) 

A matchposition(akb, 82, p4, wild, wild, com) 

A Pr[row] = Ps[row] 

A P4[COl] = Ps[COl] 

A match-turn(akb, 82, t2, opp, wild) 

A t2[count] = 1 + tl[count]) 

else blk-dia(akb, sl) = s1 
96 Appendix D. Tic-Tac-Toe Specifications 

endif ) 

blkxollhs-def: Axiom 

blkdlhs(akb, 91) 

*(3tl ,P1 ,P2 ,ps: 

match-turn(akb, 81, tl, corn, wild) 

A matchposition(akb, 81, p1, wild, wild, opp) 

A matchposition(akb, s1,p2, wild, pl[col], opp) 

A P1 [row] # P2 bowl 

A match-position(akb, $1, ps, wild, pz[col], free)) 

blkiowlhsdef Axiom 

blkrowlhs(akb, 91) 

*(% ,P1 ,P2 rP3: 

matchfurn(akb, 81, fly com, wild) 

A match-position(akb, s1,p1, wild, wild, opp) 

A match-position(akb, s1,p2,p1[row], wild, opp) 

A Pl[COl] # P2 [toll 

A match-position(akb, 81, ps, row], wild, free)) 

blkdialhs-def Axiom 

blkdialhs(akb, 91) 

*(3tl ,P1 ,P2 ,ps: 

match-turn(akb, $1, tl, corn, wild) 

A matchposition(akb, s1,pl, wild, wild, opp) 

End tttrIs3 
97 

tttils4: Module 

Using tttptypes, states, facts, kbs, sets[fact] 

Exporting blkxc, blk-cm, blkxclhs, blk-cm-lhs 

Theory 

f: VAR fact 

r,c: VAR nat 

tl, t2: VAR turn 

SI, sz: VAR state 

blk-cc: function[kb, state + state] 

blk-cm: function[kb, state -+ state] 

blk-cclhs: function[kb, state + bool] 

blk-cmlhs: function[kb, state + bool] 

blk-ccdef: Axiom 

P, PX, PI, PZ, Ps, P4, p5: VAR position 

(3tl 9 PI 9 Pz 9 PS 9 P4 : 

if match-turn(akb, SI, tl, com, 3) 

A matchposition(akb, 81, p1, wild, wild, opp) 

A matchposition(akb, s1,p~, wild, wild, opp) 

A matchposition(akb, SI, p3,2,2, com) 

A matchposition(akb, 81, p4, wild, wild, free) 

Pl[row] # Pz[row] 

A Pl[CO~] # Pz [col] 

A cornerp (pl) 

A cornerp(p2) 

A centerp(p3) 

A middlep(p4) 

A (Vpx: 

((px E kbinst(akb, SI)) 

A px[marker] # free) 

* (PX = PI 

v PX = PZ v PX = P3)) 

then blk-cc(akb, 81) = next(s1) 

A -(tl E kbinst(akb, next(s1))) 

A l(p4 E kbinst(akb, next(s1))) 

A (3t2: 

match-turn(akb, next(sl), t2, opp, wild) 
98 Appendix D. Tic-Tac-Toe Specifications 

A t2[count] = 1 + tl[count]) 

A (3~5: 

matchposition(akb, next(sl), p5, wild, wild, corn) 

A p5[row] = p4[row] 

A P~[co~] = P~[co~] 

A(vp: 

(P # P4 A P # P5) 

((p E kbinst(akb, SI)) 

e, (p E kbinst(akb, next(s1)))))) 

else blk-cc(akb, 91) = s1 

endif ) 

blk-cm-def: Axiom 

(3t1 ,PI ,PZ ,PS ,~4: 

if match-turn(akb, 91, tl, corn, 3) 

A matchposition(akb, s1,p1, wild, wild, opp) 

A match-position(akb, sl,p2, wild, wild, opp) 

A matchposition(akb, 81, ps, 2,2, corn) 

A match-position(akb, 91, p4, wild, wild, free) 

A P1 [row] # P2 [row] 

A Pl[COlI # P2[COlI 

A cornerp (PI) 

A middlep(p2) 

A cornerp(p4) 

A ((P4[IOW] = Pl[row] A P4[COl] = p2[col]) 

A pr[col] = Pl[COl])) 

v (p4[row] = p2[row] 

then blk-cm(akb, 81) = next(s1) 

A l(t1 E kbinst(akb, next(s1))) 

A i(p4 E kbinst(akb, next(s1))) 

A(3t2: 

match-turn(akb, next(sl), t2, opp, wild) 

A t2[count] = 1 + tl[count]) 

A (3~5: 

matchposition(akb, next(sl), p5, wild, wild, corn) 

A p5[row] = p4[row] 

A p5[d] = p4[d] 

A(vp: 
99 

P # P4 

(p E kbinst(akb,~l)) 3 (p E 

kbinst (akb, next(s1))))) 

else blk-cm(akb, SI) = s1 

endif ) 

blk-cclhs-def: Axiom 

blk-cclhs( akb, 91) * (3tl 9 P1 , P2 9 P3 , P4 : 

match-turn(akb, SI, tl, com, 3) 

A match-position(akb, 81, p1, wild, wild, opp) 

A matchposition(akb, s1,p2, wild, wild, opp) 

A matchposition(akb, SI, p3,2,2, com) 

A matchposition(akb, ~1,p4, wild, wild, free) 

A P1 [row] # P2 [row] 

A pl[col] # p2[col] A cornerp(p1) A cornerp(p2) A 

middlep(p4)) 

blk-cmlhsdef: Axiom 

blk -cclhs (ak b , s 1) * (3tl ,P1 ,P2 IPS 9P4: 

match-turn(akb, 81, tl, com, 3) 

A match-position(akb, 81, p1, wild, wild, opp) 

A matchposition( akb, SI, p2, wild, wild, opp) 

A matchposition(akb, SI, ps, 2,2, corn) 

A matchposition(akb, SI, p4, wild, wild, free) 

A P1 [row] # P2 [row] 

A P1 [toll # P2 [toll 

A cornerp(p1) 

A middlep(p2) 

A cornerp(p4) 

A ((P~[~ow] = ~i[row] A P~[co~] = P~[co~]) 

v (p4[row] = ~~[row] ~p,[col] = 

PWI))) 

End ttt~lsli 
100 Appendix D. Tic- Tsc- Toe Specifics tions 

guarded-ops: Module 

Ueing tttptypes, ttt_rlsl, ttt-rld, tttils3, tttils4, states, kbs 

Exporting tttap, g-winxol,g-winiow,g-windia,gblk-cc, 

ghlk-cm, ghlkxol, gblkiow, ghlk-dia, g-mkemve 

Theory 

ttt-op: TYPE from function[kb, state + state] 

g-winxol: tttap 

g-winxow: tttap 

g-windia: tttap 

g-blk-cc: tttap 

g-blk-cm: ttt-op 

g-bik-col: ttt-op 

g-blkrow: ttt_op 

g-blk-dia: ttt-op 

g-mkemve: tttap 

gop: VAR ttt-op 

an: VAR state 

g-winxoldef: Axiom 

g-win-col(akb, sn) 

= if win-collhs(akb,s,) then win-col(akb,s,) else sn end if 

g-winxowdef: Axiom 

g-winJow(akb, sn) 

= if ((iwin-collhs(akb, Sn)) A winxowlhs(akb, sn)) 

then winJow(akb, an) 

eke 8, 

end if 

g-windiadef: Axiom 

g-windia(akb, 8n) 

= if ((l(winxollhs(akb, sn) V win_rowlhs(akb, an))) 

A windialhs(akb, sn)) 

then win-dia(akb, sn) 

else 8, 

end if 
10 1. 

g-blkxc-def: Axiom 

gblk-cc(akb, s,) 

= if ((-(windlhs(akb, s,) 

A blk-cc-lhs(akb, 8,)) 

V winrowlhs(akb, s,) V windialhs(akb, s,))) 

then blkxc(akb, s,) 

else s, 

end if 

g-blkxmdef: Axiom 

gblk-cm(akb, s,) 

= if ((-(win,collhs(akb, 8,) 

V winiowlhs(akb, s,) 

V win-dialhs(akb, s,) v blk-cclhs(akb, s,))) 

A blk_collhs(akb, s,)) 

then blkxol(akb, s,,) 

else s, 

end if 

g-blk-col-def: Axiom 

gblk-col(akb, s,) 

= if ((-(win-collhs(akb, 8,) 

v winiowlhs(akb, 8,) 

V windialhs(akb, s,) 

vblkxclhs(akb, s,) vblkxmlhs(akb, 8,))) 

A blk-collhs(akb, s,)) 

then blk-col( ak b, a,,) 

else s, 

end if 

g-blk_rowdef: Axiom 

g-blk-row(akb, s,) 

= if ((-(winxollhs(akb, s,) 

V winiowlhs( akb, 8,) 

V windiaJhs(akb, s,) 

V blk-cclhs(akb, sn) 

Vblk-cmlhs(akb, s,)vblk-collhs(akb, 8,))) 
102 Appendix D. Tic- Tac- Toe Specifica tions 

A blklowlhs(akb, an)) 

then blkxow(akb, 8n) 

else an 

end if 

gblk -diadef: Axiom 

gblkdia(akb, s,,) 

= if ((-(win_collhs(akb, sn) 

V winiowlhs(akb, s,,) 

V win-dialhs(akb, 8,) 

V blk-cc-lhs(akb, an) 

V blkxmlhs(akb, an) 

Vblk-colh(akb, sn)Vblkiowlhs(akb, ~n))) 

h blk-dialhs(akb, sn)) 

then blk-dia( ak b , sn) 

else 8, 

end if 

gmkemvedef: Axiom 

gmkemve(akb, sn) 

= if ((i(win_collhs(akb, s,,) 

V win_rowlhs(akb, an) 

V windialhs(akb, an) 

V blk-cclhs(akb, an) 

V blk-cmlhs(akb, an) 

V blk -collhs (ak b , an) 

Vblk i o w l h s (ak b , sn) Vblk dialhs( akb , sn))) 

A makemovelhs(akb, sn)) 

then makemove(akb, sn) 

else an 

end if 

gop-def: Axiom 

gop = g-win-col 

v gop = g-winlow 
103 

V gop = g-windia 

v gop = gblkxc 

V gop = gblk-cm 

V gop = g-blkxol 

V gop = g-blksow V gop = ghlk-dia V gop = gmkemve 

gmmax: Axiom true 

End guarded-ops 
104 Appendix D. Tic-%- Toe Specifications 

safe-ttt: Module 

Using ttt-ptypes, kbs, states, facts, diffs 

Exporting safe, wongame, losenextmove, unsafe-config-l, 

unsafe-config2, unsafe-config3, unsafexonfig-4 

Theory 

sn,sm: VAR state 

tl, t2: VAR turn 

pl,p2,ps,p4: VAR position 

kbx: VAR kb 

won-game: function[kb, state + bool] 

losenextmove: function[kb, state + bool] 

unsafe-codgl: function[kb, state + bool] 

unsafe-config2: function[kb, state -, bool] 

unsafexonfig3: function[kb, state + bool] 

unsafe-config-4: function[kb, state + bool] 

safe: function[kb, state + bool] 

safedef: Axiom 

safe(kbx, Sn) 

won-game(kbx, sn) 

V y(losenextmove(kbx, an) 

V unsafe-config-l(kbx, an) 

V unsafeeconfig2(kbx, Sn) 

v unsafe-config-3(kbx, an) V unsafe-config-4(kbx, sn)) 

won-gamedef: Axiom 

won-game(kbx, sn) 

*((3Pl,pZ,Ps: 

matchposition(kbx, an, p1, wild, wild, com) 

A matchposition(kbx, an,-, wild, wild, corn) 

A match-position(kbx, sn, ps, wild, wild, com) 

APl#PL 

AP2 # PS 

APlZPS 

A ((P1 [coy = P2 [col] A P2 [col] = Ps [coy) 

v (pi[row] = p2[row] A p2[row] = ps[row]) 

v (cornerp(p1) 
105 

losenextmovedef: Axiom 

losenextmove(kbx, 8,) 

*(3tl,Pl ,p2,ps: 

matchfurn(kbx, s, tl, opp, wild) 

A matchposition(kbx, s,, p1, wild, wild, opp) 

A match-position(kbx, sn,p2, wild, wild, opp) 

A matchposition(kbx, s,,ps, wild, wild, free) 

APlfP2 

A ((cornerp(p1) 

A cornerp (p2) 

A centerp(p3) 

A Pr[row] # p2[rowl 

A PI [toll # P2 [toll 

v (p1[row] = p2[row] APz[row] = Ps[row]) 

v (Pl[COl] = P2[col] A Pz[col] = Ps[COl]))) 

unsafe-config-1 -def: Axiom 

unsafe-config_l(kbx, 8,) * (It1 , P1 , P2 , Ps 2 P4 : 

matchfurn(kbx, s, tl, opp, 4) 

A match-position(kbx, s, p1, wild, wild, com) 

A match-position(kbx, s,, p2, wild, wild, corn) 

h matchposition(kbx, s,, ps, wild, wild, opp) 

A matchposition(kbx, s,, p4, wild, wild, opp) 

AP1# P2 

APs#P4 

Acenterp (PI) Acornerp(p2) Acornerp (ps) Acornerp (~4)) 

unsafexonfig2def: Axiom 

unsafe-config2(kbx, 8,) 

* ( 3 tl , P1 , P2 , Ps , P4 : 

matchfurn(kbx, s,, tl, opp, 4) 
106 Appendix D. Tic-Tac-Toe Specifications 

A match-position(kbx, an, pi, wild, wild, com) 

A match_position(kbx, s,,, pz, wild, wild, com) 

A match_position(kbx, an, ps, wild, wild, opp) 

A matchposition(kbx, an, p4, wild, wild, opp) 

AP1# P2 

A Ps # P4 

Amiddlep(p1)Amiddlep(p2)Acornerp(ps)Acornerp(p4)) 

unsafexonfig3def: Axiom 

unsafe-config 3 (kbx , sn ) * (3tl Y P1 ,P2 ,Ps Y P4 : 

match-turn(kbx, s,,, tl, opp, 4) 

A match-position(kbx, Sn, p1, wild, wild, com) 

A matchposition(kbx, sn, p2, wild, wild, corn) 

A match-position(kbx, s,, ps, wild, wild, opp) 

A match-position(kbx, ~n, p4,wild, wild, opp) 

AP1# P2 

A Ps # P4 

Acornerp (PI) Acornerp (p2) Amiddlep (ps) Amiddlep (p4)) 

unsafe-config-4,def: Axiom 

unsafe-config-4(kbx, sn) * Wl ,P1 ,P2 ,Ps 9P4: 

match-turn(kbx, sn, tl, opp, 4) 

A matchposition(kbx, sn,p1, wild, wild, corn) 

A match-position(kbx, sn, p2, wild, wild, corn) 

A match-position(kbx, sn, ps, wild, wild, opp) 

A match-position(kbx, an, p4, wild, wild, opp) 

AP1# P2 

APSZP4 

A centerp(p1) 

A cornerp(pz) 

A cornerp(p3) 

A middlep(p4) 

Al( (p2 [row] = Ps [row] AP2 [.I] = P4 [col]) 
107 

End safeftt 
108 Appendix D. Tic-Tac-Toe Specifications 

initialstate: Module 

Using tttptypes, kbs, states, facts, sets(fact1 

Theory 

p,p1: VAR position 

t,tl: VAR turn 

sx: VAR state 

initial_positions: Axiom (p E kbinst(akb, SO)) e marker] = free 

initial-turn: Axiom 

(t E kbinst(akb, SO)) t[player] = opp A t[count] = 0 

End initialstate 
109 

initialproof: Module 

Using tttptypes, safe-ttt, states, kbs, initialstate 

Theory 

sis: Lemma safe(akb, SO) 

Proof 

p: VAR position 

rx, cx, mx: VAR datum 

nextmove: Lemma llosenextmove(akb, SO) 

nmp: Prove nextmove from 

losenextmovedef {kbx t akb, an t SO}, 

initialpositions {p + plQpls}, 

distinct-constants 

configl: Lemma -unsafe-config-l(akb, SO) 

clp: Prove configl from 

unsafe-config-1-def {kbx + akb, an t SO}, 

initialpositions {p + plQpls}, 

distinct-constants 

config2: Lemma -unsafe_config2(akb, SO) 

c2p: Prove config2 from 

unsafe-config2-def {kbx t akb, an + SO}, 

initialpositions {p t plOpls}, 

distinct -constants 

config3: Lemma -.lunsafe_config3(akb, SO) 

c3p: Prove config3 from 

unsafe-config-3-def {kbx t akb, sn t SO}, 

initialpositions {p t plQpls}, 

distinct -const ants 

config4: Lemma wm-mfe-configd(akb, SO) 

c4p: Prove config4 from 

unsafe-config-4-def {kbx + akb, an 

initialpositions {p + plQpIs}, 

SO}, 
110 Appendix D. Tic-TaeToe Specifications 

distinct _constants 

sisp: Prove sis from 

safedef {kbx t akb, a,, t SO}, 

next rmove, 

configl, 

config2, 

config3, 

config4 

End initialproof 
111 

gwrproof: Module 

Using guardedAps, safe-ttt, tttptypes, states, tttlls2 

Theory 

s,,: VAR state 

safe-gwrstep: Lemma safe(akb, sn) 3 safe(akb, g-winiow(akb, sn)) 

Proof 

no-transition: Lemma 

(safe(akb, s,)Ag-win_row(akb, s,) = sn) 3 safe(akb, g-win_row(akb, s,,)) 

ntp: Prove no-transition 

safe-trans: Lemma 

(safe(akb, s,,) A g-winiow(akb, sn) = next(s,)) 

3 safe(akb, g-winiow(akb, s,,)) 

stll: Lemma 

g-win_row(akb, sn) = next(s,,) 

3 (win-rowlhs(akb, s,,) A winiow(akb, sn) = next(s,,)) 

stllp: Prove stll from g-winiowdef {s,, + s,Qcs} 

st12: Lemma win_row(akb, s,,) = next(s,) 3 won_game(akb, win_row(akb, s,,)) 

stl2p: Prove st12 from 

wkrowdef {SI t s,,@cs, p t pl@lpls}, 

winlow-def (81 t s,,Qcs, p t p2Qpls}, 

wongamedef {kbx t akb, 

s,, t next(s,@cs), 

P1 +- PlQPlS, 

P2 +- PZQPlS, 

PS PlQPW, 

distinct-constants 

stpp: Prove safe-trans from 

stll {sn s,QCS}, 
112 Appendix D. Tic-&- Toe Specifications 

st12 {an + SnQCS}, 

safedef {kbx + akb, sn + win-row(akb, SnO-)} 

sgsll: Lemma winrow(akb, Sn) = sn V win-row(akb, Sn) = next(sn) 

sgsllp: Prove sgsll fiom winJow-def (81 c- an@-} 

safegwrstepproof: Prove safegwrstep from 

no-transition {an t SnQ-}, 

safe-trans {an + SnO-}, 

g-winiowdef {an + SnQcs} 

Sgsll {en + sn@cs}, 

End gwrproof 
113 

gwcproof: Module 

Using guardedaps, safe-ttt, tttptypes, states, tttils2 

Theory 

8,: VAR state 

safe-gwcstep: Lemma safe(akb, 8,) 3 safe(akb, g-win-col(akb, 8,)) 

Proof 

no-transition: Lemma 

(safe(akb, 8,) A g-win-col(akb, 9,) = 9,) 3 safe(akb, g-win-col(akb, s,)) 

ntp: Prove no-transition 

safe-trans: Lemma 

(safe(akb, 8,) A g-win-col(akb, 8,) = next(s,)) 

3 safe(akb, g-win-col(akb, 9,)) 

stll: Lemma 

g-win-col(akb, s,) = next(s,) 

3 (win-collhs(akb, s,) A win-col(akb, 8,) = next(s,)) 

stllp: Prave stll &om g-win-coldef {s, t s,Qcs} 

st12: Lemma win-col(akb, 8,) = next(s,) 3 won-game(akb, winxol(akb, 8,)) 

stl2p: Prove st12 fkom 

winxoldef {SI t s,Qcs, p t plQpls}, 

winxoldef (81 + snQcs, p t prQpls}, 

won-gamedef {kbx t akb, 

s, t next(s,Qcs), 

P1 PlQPlS, 

P2 P2QPlS9 

PS P4QPW, 

distinctxonstants 

stpp: Prove safe-trans from 

stll (8, t s,QCS}, 
114 Appendix D. Tic-Tac-Toe Specifications 

st12 {Sn + s~QCS}, 

safedef {kbx akb, 8, + win-col(akb, Sn&S)} 

sgsll: Le- win-col(akb, 8,) = v winZol(akb, sn) = next(s,) 

sgsllp: Prove sgsll from win-coldef {SI t s,Qcs} 

safegwcstep-proof: Prove safe-gwcstep from 

no-transition {s, t s,Qcs}, 

safe-trans {an + SnQa}, 

g-win-col-def {an t- S,QCS} 

sgsll {sn + snQcs}, 

End gwc-proof 
115 

gwd-proof: Module 

Using guarded-ops, safe-ttt, tttptypes, states, tttild 

Theory 

s,,: VARstate 

safe-gwdstep: Lemma safe(akb, sn) 3 safe(akb, g-windia(akb, s,,)) 

Proof 

no-transition: Lemma 

(safe(akb, s,,)Ag-windia(akb, s,,) = sn) 3 safe(akb, g-windia(akb, sn)) 

ntp: Prove no-transition 

safe-trans: Lemma 

(safe(akb, sn) A g-windia(akb, s,,) = next(s,)) 

3 safe(akb, g-windia(akb, sn)) 

stll: Lemma 

g-win-dia(akb, sn) = next(s,) 

3 (windialhs(akb, s,,) A windia(akb, sn) = next(s,)) 

stllp: Prove stll from g-windiadef {s,, t s,Qcs} 

st12: Lemma windia(akb, s,,) = next(s,,) 2 won-game(akb, windia(akb, s,,)) 

stl2p: Prove st12 from 

windiadef (81 t s,,@cs, p e plQpls}, 

windia-def (81 t s,,Qcs, p t p2Qpls}, 

won-gamedef {kbx t akb, 

s,, t next (s,Qcs), 

Pl PlQPlS, 

P2 +- PtQPlS, 

PS PrQPlSI, 

distinct-constants 

stpp: Prove safefrans from 

stll {sn + s,QCS}, 
116 Appendix D. Tic- Tac- Toe Specifications 

st12 {an + SnQCS}, 

safedef {kbx + akb, 8, + windia(akb, an@cs)} 

sgsll: Lemma windia(akb, an) = an V windia(akb, an) = next(an) 

sgsllp: Prove sgsll from windiadef {SI t anOcs} 

safegwdstep-proof: Prove safeqdstep from 

no-transition {Sn + SnQm}, 

safe-trans {an + an@=}, 

g-windiadef { Sn + SnQcs} 

sgsll {an + an@=}, 

End gwdproof 
Appendix E 

Backward-Chaining System 

(def un remember (new) 

"Places a fact on the *facts* list if it is not already there." 

(cond ((member new *facts* :test #'equal) nil) 

(t (setf *facts* (cons new *facts*) 1 

new) 1) 

(defun recall (fact) 

"Tests to see if a fact is already asserted on the *facts* list." 

(cond ((member fact *facts* :test #'equal) fact) 

(t nil) 1) 

(defun failed (fact) 

"Tests to see if a previous attempt to assert the fact failed." 

(cond ((and (not (recall fact) 1 

(member fact *asked* :test #'equal) 

t) 

(t nil) 1) 

(defun testif+ (rule) 

can be satisfied. " "Attempts to verify if each condition in the ifs clause 

(prog (ifs) 

(setf ifs (cdaddr rule)) 

(return 

117 
118 Appendix E. Backward-Chaining System 

(loop 

(cond ((null if s) (return t)) 

((if (eql (caar ifs) 'not) 

(verify (car ifs))) 

(setf ifs (cdr ifs))) 

(t (return nil) 1) 1) 1) 

(not (verify (cadar if s) 

(defun testif (rule) 

"Tests to see if each conditions in the ifs clause 

(prog (ifs) 

has already been asserted." 

(setf ifs (cdaddr rule)) 

(return 

(loop 

(cond ((null ifs)(return t)) 

((if (eql (caar ifs) 'not) 

(recall (car ifs))) 

(setf ifs (cdr ifs))) 

(t (return nil) 1) 1) 1) 

(failed (cadar ifs)) 

(defun inthen (fact) 

"Returns a list of rules for which fact occurs on the RHS.'l 

(mapcan #' (lambda (r) 

(cond ((thenp fact r) 

(list r) 1) 1 

*rules*) 1 

(defun thenp (fact rule) 

"Test to see if a fact is in the RHS of a rule.If 

(member fact (cadddr rule) :test #'equal)) 

(defun usethen (rule) 

IvAsserts the RHS of a rule whose LHS has been justified." 

(let ((thens (cdr (cadddr rule))) (success nil)) 

(loop 

(cond ((null thens) (return success)) 

((remember (car thens)) 
119 

(format t "-%Rule <'A>'%'tdeduces: -An 

(cadr rule) (car thens) ) 

(setf success t) 

(setf thens (cdr thens))))) ) ) 

(defun tryrule (rule) 

"Attempts to use a rule." 

(and (testif rule) (usethen rule)) ) 

(defun tryrule+ (rule) 

"Attempts to use a rule. 

(and (testif + rule) (usethen rule) 1) 

Uses a recursive call to verify." 

(defmacro get-question (fact) 

'(cadr (assoc fact *questions* :test #'equal))) 

(defun verify (fact) 

"Main procedure which attempts to establish a fact." 

(pro8 (ri r2) 

(cond ((recall fact)(return t))) 

(setf rl (inthen fact)) 

(setf r2 rl) 

(if (null ri) 

(cond ((member fact *asked* :test #'equal) (return nil) 1 

((yes-or-no-p "-%-A?" (get-question fact)) 

(remember fact ) 

(return t ) ) 

(t (setf *asked* (cons fact *asked*)) 

(return nil) 1) ) 

loopl 

(cond ((null rl) 

(go loop2)) 

(return t) 1) 

((tryrule (car ri)) 

(setf r1 (cdr ri)) 

(go loopl) 

loop2 

(cond ((null r2) (go exit)) 

((tryrule+ (car r2)) 
120 Appendix E. Backward-Chaining System 

(return t))) 

(setf r2 (cdr r2)) 

(go loop2) 

exit 

(return nil))) 

(defun diagnose 0 

"Top level function which conducts diagnosis.Il 

(let ((pos *hyps*)(*asked* nil)(*facts* nil)) 

(declare (special *asked* *facts*)) 

(loop 

(cond ((null pos) 

(format t "'%No diagnosis available.") 

(return nil)) 

(format t n-7giagnosis: 'A. (car pos)) 

(return (car pas>)>> 

((verify (car pos)) 

(setf pos (cdr pas)>>>> 

(defvar *rules* nil 

"The list of current rules in the system.") 

(defmacro define-rule (&rest rulebody) 

ing to type in one long list of rules." 

"A macro to make typing in rules more intuitive --Avoids hav- 

'(setf *rules* 

(append *rules* 

(list (cons 'rule ' , rulebody)) 1) 

(def var *questions* nil 

"The list of queries to establish ground facts.") 

(def macro phrase-question (fact question) 

ate facts more intuitive." 

"A macro to make typing in questions to be used to substanti- 

'(setf *questions* 

(cons (list ' ,fact .question) 

*questions*) 1) 
121 

(defun initialize (1 

(setf *rules* nil) 

(setf *questions* nil) 1 

(defmacro hypothesis (hest hlist) 

"A macro to make entering hypothesis more intuitive." 

'(setf *hyps* '.hlist)) 
122 Appendix E. Backward- Chaining System 
Appendix F 

Heuristics for Electrical 

System Diagnosis 

... 

1.1 

;;; small rnle base for diagnosis of problems in an automobile 

;;; electrical system. ... 

DII 

(initialize 1 

(def ine-rule rl 

(if (engine wont start) 

(starter doesnt turn) 

(bad battery) ) 

(then (replace or repair battery))) 

(phrase-question (engine wont start) 

IIDoes the engine FAIL to start") 

(phrase-question (starter doesnt turn) 

IIDoes the starter motor FAIL to turnn) 

(define-rule r2 

(if (engine wont start) 

(starter doesnt turn) 

(not (bad battery)) 

(jump solenoid starter turns) 
124 Appendix F. Heuristics for Electrical System Diagnosis 

(bad ignition) 1 

(then (replace or repair ignition))) 

(phrase-question (jump solenoid starter turns) 

"Does the starter turn normally when a jumper is connected 

across the battery and starter posts of the solenoid") 

(def ine-rule r3 

(if (engine wont start) 

(starter doesnt turn) 

(not (bad battery) 1 

(not (bad ignition) 

(jump solenoid no response) 

(then (replace or repair solenoid) ) 1 

(phrase-question (jump solenoid no response) 

"Does the starter FAIL to turn at all when a jumper is 

connected across the battery and starter posts of the solenoid") 

(def ine-rule r4 

(if (engine wont start) 

(starter doesnt turn) 

(not (bad battery) ) 

(jump solenoid starter turns)) 

(then (replace or repair starter) 1) 

(def ine-rule r6 

(if (engine wont start) 

(starter doesnt turn) 

(jump solenoid starter buzzes)) 

(then (replace or repair starter))) 

(phrase-question (jump solenoid starter buzzes) 

"Does the starter buzz or turn very slowly when a jumper 

is connected across the battery and starter posts of the 

solenoid") 

(def ine-rule r6 
(if (battery case cracked)) 

(then (bad battery) 1) 

(phrase-question (battery case cracked) 

"Is the battery case cracked") 

(def ine-rule r7 

(if (battery connections corroded)) 

(then (bad battery))) 

(phrase-quest ion (battery connect ions corroded) 

"Are the battery clamps and posts corrodedH) 

(def ine-rule r8 

(if (battery cells low)) 

(then (bad battery))) 

(phrase-question (battery cells low) 

"1s the state of charge in any of the cells lower 

than normal") 

(def ine-rule 1-9 

(if (no power at ignition)) 

(then (bad ignition) 1) 

(phrase-question (no power at ignition) 

nDoes the needle of a voltmeter connected to the start 

post of the solenoid fail to move when the key is jiggledH) 

(def ine-rule rlO 

(if (flickers at ignition)) 

(then (bad ignition))) 

(phrase-question (flickers at ignition) 

"Does the needle of a voltmeter connected to the start post 

of the solenoid flicker when the key is jiggledH) 

(hypothesis 

(replace or repair battery) 

125 
126 Appendix F. Heuristics for Electrical System Diagnosis 

(replace or repair ignition) 

(replace or repair solenoid) 

(replace or repair starter)) 
Appendix G 

Derived Expert System 

Rules for Diagnosis 

.. 

11 

;; simple expert system rule set for diagnosis of problems 

;; in a car's electrical system. .. 

11 

(initialize) 

(def ine-rule dl 

(if (power at cells)) 

(then (power at battery))) 

(def ine-rule dla 

(if (cell levels normal)) 

(then (power at cells))) 

(phrase -que st ion (cell levels normal) 

"Are all of the voltage levels of the individual battery 

cells normal") 

(def ine-rule d2 

(if (power at battery) 

(good battery) 

(then (power at ignition) 1) 

127 
128 Appendix G. Derived Expert System Rules for Diagnosis 

(def ine-rule d2a 

(if (not (bad battery case)) 

(then (good battery) 

(not (bad battery connections) 1) 

(phrase-question (bad battery case) 

"Are there any cracks or damage to the battery casett) 

(phrase -quest ion (bad battery connections 

"Are the battery posts and cable clamps corrodedtt) 

(def ine-rule d3 

(if (power at ignition) 

(good ignition)) 

(then (power at points) 

(power at solenoid))) 

(def ine-rule d3a 

(if (not (open ignition switch)) 

(then (good ignition) ) ) 

(not (sporadic ignition) ) ) 

(phrase-question (open ignition switch) 

"Does a voltmeter connected to the starter post of the 

(phrase -quest ion (sporadic ignition) 

ItDoes the needle of a voltmeter flicker when the key is 

solenoid fail to move when the key is turned to the start positiontt) 

j iggledtt) 

(def ine-rule d4 

(if (power at points) 

(good points) ) 

(then (power at coil))) 

(def ine-rule d4a 

(if (not (point gap off)) 

(then (good points)) 

(not (damaged points) 1) 
(phrase-question (point gap off ) 

"Does a dwell meter indicate the point gap needs adjusting") 

(phrase-question (damaged points) 

"Do the points show pitting, excessive wear, or other signs 

of damage") 

(def ine-rule d6 

(if (power at coil) 

(good coil)) 

(then (power at distributor) 1) 

(def ine-rule d6a 

(if (good primary coil resistance) 

(then (good coil))) 

(good secondary coil resistance)) 

(phrase-question (good primary coil resistance) 

"Does an ohmmeter indicate from 1 to 4 ohms of resistance 

(phrase-question (good secondary coil resistance) 

"Does an ohmmeter indicate from 4,000 to 10,000 ohms of 

in the primary coil") 

resistance in the secondary coil") 

(def ine-rule d6 

(if (power at distributor) 

(good distributor) ) 

(then (power at plugs))) 

(def ine-rule d6a 

(if (not (bad distributor cap))) 

(then (good distributor)) 

(phrase-question (bad distributor cap) 

"Does the distributor cap and rotor show signs of burning 

or corrosion") 

(def ine-rule d7 

(if (power at solenoid) 

(good solenoid)) 

129 
130 Appendix G. Derived Expert System Rules for Diagnosis 

(then (power at Starter) 

(def ine-rule d7a 

(if (jumped solenoid tarns normal) 

(then (good solenoid) ) ) 

(phrase-question (jumped solenoid turns normal) 

"Does the starter turn normally when a jumper is connected 

between the battery and starter posts of the solenoidI1) 

(def ine-rule d7b 

(if (jumped solenoid starter buzz)) 

(then (good solenoid))) 

(phrase-question (jumped solenoid starter buzz) 

"Does the starter buzz or turn the engine slowly when a jumper 

is connected between the battery and starter posts of the 

solenoid") 

(def ine-rule d7c 

(if (not (jumped solenoid no response))) 

(then (good solenoid) ) ) 

(phrase-question (jumped solenoid no response) 

"Does the starter show no response when a jumper is connected 

between the battery and starter posts of the solenoid") 

(def ine-rule d8 

(if (car fails to start) 

(then (no start))) 

(starter does not turn)) 

(phrase-question (car fails to start) 

"Does your car fail to start") 

(phrase-question (starter does not turn) 

llDoes the starter fail to turn when the key is engaged") 

(define-rule yl 

(if (car fails to start) 
(not (starter does not turn)) 

(power at battery) 

(power at ignition) 

(power at points) 

(power at coil) 

(power at distributor) 

(power at plugs) 

(not (good plugs) 1) 

(then (replace plugs) ) ) 

(phrase-question (good plugs) 

"Are the spark plugs undamagedll) 

(define-rule y2 

(if (car fails to start) 

(not (starter does not turn)) 

(power at battery) 

(power at ignition) 

(power at points) 

(power at coil) 

(power at distributor) 

(not (good distributor) ) ) 

(then (replace distributor))) 

(define-rule y3 

(if (car fails to start) 

(not (starter does not turn)) 

(power at battery) 

(power at ignition) 

(power at points) 

(power at coil) 

(not (good coil) 1) 

(then (replace coil) 1) 

131 

(def ine-rule y4 

(if (car fails to start) 

(not (starter does not turn)) 

(power at battery) 

(power at ignition) 
132 Appendix G. Derived Expert System Rules for Diagnosis 

(power at points) 

(not (good points) 1) 

(then (replace points)) 

(def ine-rule y6 

(if (car fails to start) 

(starter does not turn) 

(power at battery) 

(power at ignition) 

(not (good ignition))) 

(then (replace ignition))) 

(def ine-rule y6 

(if (car fails to start) 

(starter does not turn) 

(power at battery) 

(not (good battery) 1) 

(then (replace battery) 1) 

(def ine-rule y7 

(if (car fails to start) 

(starter does not turn) 

(not (power at battery) 1 ) 

(then (replace battery) 1) 

(def ine-rule y8 

(if (car fails to start) 

(starter does not turn) 

(power at battery) 

(power at ignition) 

(power at solenoid) 

(power at starter) 

(not (good starter) 1) 

(then (replace starter) 1) 

(phrase-question (good starter) 

"Does the starter meet specifications when removed 

and bench tested") 
133 

(def ine-rule y!J 

(if (car fails to start) 

(starter does not turn) 

(power at battery) 

(power at ignition) 

(power at solenoid) 

(not (good solenoid) ) ) 

(then (replace solenoid) ) ) 

(hypo t he s is 

(replace starter) 

(replace solenoid) 

(replace plugs) 

(replace distributor) 

(replace coil) 

(replace points) 

(replace ignition) 

(replace battery) 1 
134 Appendix G. Derived Expert System Rules for Diagnosis 
Appendix H 

Electrical System Formal 

Specification 

135 

I 
136 Appendix H. Electrical System Formal Specification 

components: Module 

Exporting battery, cells, ignition, points, coil, distributor, 

Theory 

component: TYPE 

battery, cells, ignition, points, coil, distributor, plugs, solenoid, 

c: VAR component 

enum: Axiom 

plugs, solenoid, starter, component 

starter: component 

(V c: c = battery 

V c = cells 

v c = ignition 

v c = points 

V c = coil 

vc = distributorvc = plugsvc = solenoidvc = starter) 

unique: Axiom 

battery # cells 

A battery # ignition 

A battery # points 

A battery # coil 

A battery # distributor 

A battery # plugs 

A battery # solenoid 

A battery # starter 

A cells # ignition 

A cells # points 

A cells # coil 

A cells # distributor 

A cells # plugs 

A cells # solenoid 

A cells # starter 

A ignition # points 

A ignition # coil 

A ignition # distributor 

A ignition # plugs 

. 
137 

A ignition # solenoid 

A ignition # starter 

A points # cod 

A points # distributor 

A points # plugs 

A points # solenoid 

A points # starter 

A cod # distributor 

A cod # plugs 

A coil # solenoid 

A cod # starter 

A distributor # plugs 

A distributor # solenoid 

A distributor # starter 

A plugs # solenoid 

A plugs # starter 

A solenoid # starter 

End components 
, 

138 Appendix H. Electrical System Formal Specification 

enginemodel: Module 

Using components 

Exporting powerat, good 

Theory 

cl , c2: VAR component 

powerat: function[component + bool] 

good: function[component boo11 

elect ricals y s t emmodel: Axiom 

(powerat(battery) good(cells)) 

A (power at (ignition) * powerat (battery) A good(b8ttery)) 

A (powerat(points) powerat(ignition) A good(ignition)) 

A (powerat(coi1) -s powerat(points) A good(points)) 

A (powerat(distributor) powerat(coi1) h good(coi1)) 

A(power at (plugs) 0 powerat (distributor) Agood( distributor)) 

A (power at( solenoid) e powerat (ignition) Agood( ignition)) 

A (power at (starter) e power at (solenoid) Agood( solenoid)) 

singlefailure: Axiom lgood(c1) 3 (Vc2: c2 # cl 3 good(c2)) 

Proof 

testl: Lemma ygood(coi1) 3 lpowerat(distribut0r) A 'power-at(p1ugs) 

tlp: Prove testl from electricalsystemmodel 

test2: Lemma -.power-at(ignition) 3 lpower-at(starter) 

t2p: Prove test2 from electricalsystemmodel 

test3: Lemma powerat(coi1) 3 powerat(battery) A good(ignition) 

t3p: Prove test3 from electricalsystemmodel 

End enginemodel 
139 

test: Module 

Using components, enginemodel 

Theory 

batt: Lemma powerat(battery) 

igni: Lemma powerat(igniti0n) 

poin: Lemma powerat (points) 

coil: Lemma power-at(coi1) 

dist : Lemma power at (distributor) 

plug: Lemma powerat(p1ugs) 

sole: Lemma powerat(so1enoid) 

star: Lemma powerat(starter) 

End test 
140 Appendix H. Electrical System Formal Specification 

predict: Module 

Using components, enginemodel, test 

Theory 

comp: component = solenoid 

cause: Axiom igood(comp) 

Proof 

powerat-batt: Prove test.batt from 

cause, 

electricalsystemmodel, 

unique, 

singlefailure {cl t comp, c2 t cells}, 

singlefailure {cl + comp, c2 + battery}, 

singlefailure {cl t comp, c2 + ignition}, 

singlefailure {cl t comp, c2 t points}, 

singlefailure {cl + comp, c2 + components.coil}, 

singlefailure {cl t comp, c2 +- distributor}, 

singlefailure {cl t comp, c2 t plugs}, 

singlefailure {cl t comp, c2 t solenoid}, 

singlefailure {cl + comp, c2 + starter} 

poweratigni: Prove test.igni from 

cause, 

electricalsystemmodel, 

unique, 

singlefailure {cl t comp, c2 t cells}, 

singlefailure {cl t comp, c2 t battery}, 

singlefailure {cl + comp, c2 + ignition}, 

singlefailure {cl t comp, c2 t points}, 

singlefailure {cl t comp, c2 t components.coil}, 

singlefailure {cl t comp, c2 t distributor}, 

singlefailure {cl + comp, c2 + plugs}, 

singlefailure {cl t comp, c2 t solenoid}, 

singlefailure {cl t comp, c2 t starter} 

powerat-poin: Prove test.poin from 

cause, 

electricalsystemmodel, 
unique, 

singlefailure {cl t comp, c2 t cells}, 

singlefailure {cl t comp, c2 + battery}, 

singlefailure {cl + comp, c2 + ignition}, 

singlefailure {cl t comp, c2 t points}, 

singlefailure {cl +- comp, c2 + components.coil}, 

singlefailure {cl t comp, c2 t distributor}, 

singlefailure {cl + comp, c2 + plugs}, 

singlefailure {cl t comp, c2 t solenoid}, 

singlefailure {cl t comp, c2 t starter} 

poweratxoil: Prove test .coil from 

cause, 

electricalsystemmodel, 

unique, 

singlefailure {cl t comp, c2 t cells}, 

singlefailure {cl 4- comp, c2 t battery}, 

singlefailure {cl + comp, c2 t ignition}, 

singlefailure {cl t comp, c2 t points}, 

singlefailure {cl t comp, c2 t components.coil}, 

singlefailure {cl t comp, c2 t distributor}, 

singlefailure {cl t comp, c2 t plugs}, 

singlefailure {cl + comp, c2 t solenoid}, 

singlefailure {cl +- comp, c2 t starter} 

power-atdist: Prove test.dist from 

cause, 

electricalsystemmodel, 

unique, 

singlefailure {cl t comp, c2 t cells}, 

singlefailure {cl t comp, c2 t battery}, 

singlefailure {cl t comp, c2 t ignition}, 

singlefailure {cl + comp, c2 t points}, 

singlefailure {cl t comp, c2 t components.coil}, 

singlefailure {cl +- comp, c2 

singlefailure {cl + comp, c2 t plugs}, 

singlefailure {cl t comp, c2 t solenoid}, 

singlefailure {cl + comp, c2 t starter} 

distributor}, 

power-atplug: Prove test.plug from 

141 
142 Appendix H, Electrical System Formal Specification 

cause, 

electricalsystemmodel, 

unique, 

singlefailure {cl t comp, c2 t cells}, 

singlefailure {cl + comp, c2 + battery}, 

singlefailure {cl t comp, c2 t ignition}, 

singlefailure {cl + comp, c2 + points}, 

singlefailure {cl t comp, c2 +- components.coil}, 

singlefailure {cl t comp, c2 t distributor}, 

singlefailure {cl t comp, c2 t plugs}, 

singlefailure {cl t comp, c2 t solenoid}, 

singlefailure {cl + comp, c2 t starter} 

poweratsole: Prove test.sole from 

cause, 

electricalsystemmodel, 

unique, 

singlefailure {cl t comp, c2 t cells}, 

singlefailure {cl + comp, c2 + battery}, 

singlefailure {cl t comp, c2 t ignition}, 

singlefailure {cl + comp, c2 +- points}, 

singlefailure {cl t comp, c2 t components.coil}, 

singlefailure {cl + comp, c2 t distributor}, 

singlefailure {cl t comp, c2 t plugs}, 

singlefailure {cl 

singlefailure {cl t comp, c2 t starter} 

comp, c2 + solenoid}, 

poweratstar: Prove teststar from 

cause, 

electricalsystemmodel, 

unique, 

singlefailure {cl t comp, c2 t cells}, 

singlefailure {cl t comp, c2 t battery}, 

singlefailure {cl t comp, c2 t ignition}, 

singlefailure {cl t comp, c2 t points}, 

singlefailure {cl +- comp, c2 t components.coil}, 

singlefailure {cl t comp, c2 t distributor}, 

singlefailure {cl t comp, c2 t plugs}, 

singlefailure {cl t comp, c2 t solenoid}, 

singlefailure {cl t comp, c2 t starter} 
143 

End predict 
144 Appendix H. EIectrical System Formal Specification 
Bibliography 

[ 11 Introduction to EHDM. Computer Science Laboratory, SRI International, Menlo Park, CA 94025, September 28, 1988. 

[2] EHDM Specification and Verification System Version 4.1-Preliminary 

Definition of the EHDM Specification Language. Computer Science 

Laboratory, SRI International, Menlo Park, CA 94025, September 6, 

1988. 

[3] EHDM Specification and Verification System Version 4.1-User’s 

Guide. Computer Science Laboratory, SRI International, Menlo Park, 

CA 94025, November 29, 1988. 

[4] B. Alpern and F.B. Schneider. Defining liveness. Information Processing Letters, 21(4):181-185, October 1985. 

[5] Debra Anderson and Charles Ortiz. AALPS: a knowledge-based system 

for aircraft loading. IEEE Ezpert, 2(4):71-79, Winter 1987. 

[6] A. Avi3ienis and J.C. Laprie. Dependable computing: from concepts 

to design diversity. Proceedings of the IEEE, 74(6):629-638, May 1986. 

[7] H. P. Barendregt. The Lambda Calculus, its Syntaz and Semantics. 

North-Holland, Amsterdam, 1978. 

[8] William R. Bevier. Kit: A Study in Operating System Verification. 

Technical Report 28, Computational Logic Incorporated, Austin, TX, 

August 1988. 

[9] Marc Bezem. Consistency of rulebased expert systems. In 9th International Conference on Automated Deduction (CADE-9), pages 151-161, 

Springer-Verlag Lecture Notes in Computer Science Vol. 310, Argonne, 

IL, 1988. 

145 
146 Bibliography 

[lo] Daniel G. Bobrow, editor. Qualitative Reasoning about Physical Systems. The MIT Press, Cambridge, MA., 1986. 

[ll] Bruce G. Buchanan and Reid G. Smith. Fundamentals of expert systems. In Joseph F. naub, Barbara J. Grosz, Butler W. Lampson, and 

Nils J. Nilsson, editors, Annual Review of Computer Science, Volume 

3, pages 23-58, Annual Reviews, Inc., Palo Alto, CA., 1988. 

[12] S. Cha, N.G. Leveson, T.J. Shimeall, and J.C. Knight. An empirical 

study of software error detection using self-checks. In Digest of Papers, 

FTCS 17, pages 156-161, IEEE Computer Society, Pittsburgh, PA., 

July 1987. 

[13] William F. Clocksin and Christopher S. Mellish. Programming in Prolog. Springer-Verlag, New York, NY., 1981. 

[14] A.J. Cohn. Correctness properties of the Viper block model: the second 

level. In G. Birtwistle, editor, Proceeding8 of the 1988 Design Verification Conference, Springer-Verlag, 1989. Also published as University 

of Cambridge Computer Laboratory Technical Report No. 134. 

[15] A.J. Cohn. A proof of correctness of the Viper microprocessor: the 

first level. In G. Birtwistle and P.A. Subrahmanysm, editors, VLSI 

Specification, Verification and Synthesis, pages 27-72, Kluwer, 1988. 

[16] P.T. Cox and T. Pietrzykowski. Causes for events: their computation 

and applications. In 8th International Conference on Automated Deduction (CADE-81, pages 608-621, Springer-Verlag Lecture Notes in 

Computer Science Vol. 230, Oxford, England, 1986. 

[17] P.T. Cox and T, Pietrzykowski. General diagnosis by abductive 

inference. In Proceedings 1987 Symposium on Logic Programming, 

pages 183-189, IEEE Computer Society, San Francisco, CA., August 

1987. 

[18] Randall Davis and Walter Hamscher. Model-based reasoning: troubleshooting. In Howard E. Shrobe, editor, Ezploring Artificial Intelligence: Survey Talks from the National Conferences on Artificial Intelligence, chapter 8, pages 297-346, Morgan Kaufmann Publishers, Inc, 

San Mateo, CA., 1988. 
Bibliography 147 

[19] Saumya K. Debray and Prateek Mishra. Denotational and operation 

semantics for Prolog. Journal of Logic Programming, 5( 1):61-91, March 

1988. 

[20] E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, NJ, 1976. 

[21] Dave E. Eckhardt, Jr. and Larry D. Lee. A theoretical basis for the 

analysis of multiversion software subject to coincident errors. IEEE 

Transactions on Software Engineering, SE-11(12):1511-1517, December 

1985. 

[22] Im Flannagan. The consistency of negation as failure. The Journal of 

Logic Programming, 3(2):93-114, July 1986. 

[23] Charles L. Forgy. OPS5 User’s Manual. Technical Report CMU-CS81-135, Department of Computer Science, Carnegie-Mellon University, 

Pittburgh, PA., July 1981. 

[24] Michael R. Genesereth and Nils J. Nilsson. Logical Foundations of 

Artificial Intelligence. Morgan Kaufmann Publishers Inc., Los Altos, 

CA., 1987. 

[25] Allen Ginsberg. Knowledge-base reduction: a new approach to checking knowledge-bases for inconsistency and redundancy. In Proceedings, 

AAAI 88 (Volume 21, pages 585-589, Saint Paul, MN., August 1988. 

[26] Joseph A. Goguen and Timothy Winkler. Introducing OBJ. Technical Report SRI-CSL-88-9, Computer Science Laboratory, SRI Intern* 

tional, Menlo Park, CA., August 1988. 

[27] M.J.C. Gordon. Mechanizing Programming Logics in Higher Order 

Logic. Technical Report CCSRC-006, SRI International, Cambridge 

Computer Science Research Centre, Suite 23, Millers Yard, Mill Lane, 

Cambridge CB2 lRQ, England, September 1988. 

[28] Paul Harmon and David King. Ezpert Systems: Artificial Intelligence 

in Business. John Wiley and sons, New York, NY., 1985. 

[29] C. A. R. Hoare. An axiomatic basis for computer programming. Comm. 

ACM, 12(10):576-583,1969. 
148 Bibliography 

[30] Warren A. Hunt, Jr. The Mechanical Verification of a Microprocessor Design. Technical Report 6, Computational Logic Incorporated, 

Austin, TX, 1987. 

[31] J.C. King. Symbolic execution and program testing. Communications 

of the ACM, 19(7):385-394, July 1976. 

[32] J.C. Knight and N.G. Leveson. An experimental evaluation of the assumption of independence in multiversion programming. IEEE Transactions on Software Engineering, SE-12( 1):96-109, January 1986. 

I331 D.E. Knuth and P.B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, 

pages 263-293, Pergamon, New York, NY., 1970. 

[34] Wm Leler. Constraint Programming Languages: Their Specification 

[35] Nancy G. Leveson. Software safety: Why, what and how. ACM Computing Surveys, 18(2):125-163, June 1986. 

[36] A. Lew. Proof of correctness of decision table programs. Computer 

Journal, 27(3):230-232,1984. 

[37] B. Littlewood and D.R. Miller. A conceptual model of multi-version 

software. In Digest of Papers, FTCS 17, pages 150-155, IEEE Computer Society, Pittsburgh, PA, July 1987. 

and Generution. Addison-Wesley, Reading, MA., 1988. 

[38] R. Maes and J.E.M. van Dijk. On the role of ambiguity and incompleteness in the design of decision tables and rule-based systems. Computer 

Journal, 31(6):481-489,1988. 

[39] J Strother Moore. A Mechanically Verified Language Implementation. 

Technical Report 30, Computational Logic Incorporated, Austin, TX, 

September 1988. 

[40] L. Moser, P.M. Melliar-Smith, and R. Schwartz. Design Verification 

of SIFT. Contractor Report 4097, NASA Langley Research Center, 

Hampton, VA., September 1987. 

[41] Dana S. Nau and James A. Reggia. Relationships between deductive 

and abductive inference in knowledge-based diagnostic problem solving. 

In Larry Kerschberg, editor, Ezpert Database Systems, pages 549-558, 

Benjamin Cummings, 1986. 
Bibliography 149 

[42] Tin A. Nguyen, Walton A. Perkins, Thomas J. Ldey, and Deanne Pecora. Knowledge base verification. AI Magazine, 8(2):65-79, Summer 

1987. 

[43] David L. Parnas. Software aspects of strategic defense systems. American Scientist, 73(5):432-440, September-October 1985. 

[44] D.A. Pearce. The induction of fault diagnosis systems from qualitative 

models. In Proceedings, AAAI 88 (Volume l), pages 353-357, Saint 

Paul, MN., August 1988. 

[45] Harry E. Pople, Jr. On the mechanization of abductive logic. In Proceedings 3rd IJCAI, pages 147-152, Stanford, CA., August 1973. 

[46] Raymond Reiter. A theory of diagnosis from first principles. Artificial 

Intelligence, 32:57-95,1987. 

[47] Barry K. Rosen. Tree-manipulating systems and Church-Rosser theorems. Journal of the ACM, 20(1):160-187, January 1973. 

[48] John Rushby. Quality measures and Assurance for AI Software. Technical Report SRI-CSG88-7R, Computer Science Laboratory, SRI International, Menlo Park, CA., September 1988. (Final Report for SRI 

Project 4616, Task 5, NASA Contract NSAl 17067), also available as 

NASA Contractor Report 4187. 

[49] Jospeh R. Shoenfield. Mathematical Logic. Addison- Wesley, Reading, 

MA., 1967. 

(501 Robert E. Shostak. An EDcient Decision Procedure for Arithmetic Unth 

Function Symbole. Technical Report CSL-65, Computer Science Lab, 

SRI International, September 1977. 

[51] Robert E. Shostak. On the SUP-INF method for proving Presburger 

formulas. Journal of the ACM, 24(4):529-543, October 1977. 

[52] Mark E. Stickel. A Prolog-like Inference System for Computing 

Minimum- Cost Abductive Explanations in Natural-Language Interpretation. Technical Note 451, Artificial Intelligence Center, SRI International, Menlo Park, CA., September 1988. Also presented at the 

International Computer Science Conference '88, Hong Kong, December 

1988. 
I 

150 Bibliography 

[53] Motoi Suwa, A. Carlisle Scott, and Edward H. Shortliffe. An approach 

to verifying completeness and consistency in a rule-based expert system. 

AI Magazine, 3(4):16-21, Fall 1982. 

[54] Alan F. Turner, editor. Chilton’s Import Car Repair Manual 1983. 

Chilton Book Company, Chilton Way, Radnor, PA, 1982. 

[55] F.W.von Henke, J.S. Crow, R. Lee, J.M. Rushby, and R.A. Whitehurst. 

The EHDM verification environment: an overview. In Proceedings 11th 

National Computer Security Conference, pages 147-155, NBS/NCSC, 

Baltimore, MD., October 1988. 

[56] Patrick Henry Winston and Berthold Klaus Paul Horn. LISP. Addison 

Wesley, Reading, Massachusetts, 1 edition, 1981. ISBN 0-201-083299. 
Report Documentation Page 

1. Report No. 

NASA CR-181827 

3. Recipient's Catalog No. 

5. Report Date 

February 28, 1989 

6. Performing Organization Code 

2. Government Accession No. 

Expert Systems 

Constraint Satisfaction 

Model Inversion 

I 

4. Title and Subtitle 

Subject Category 61 

Formal Verification of AI Software 

7. Authodsl 

John Rushby, R. Alan Whitehurst 

9. Performing Organization Name and Address 

SRI International 

333 Ravenswood Ave. 

Menlo Park, CA 94025 

2. Sponsoring Agency Name and Address 

National Aeronautics and Space Administration 

Langley Research Center 

Hampton, VA 23665-5225 

5. Supplementary Notes 

8. Performing Organization Report No. 

10. Work Unit No. 

549-03-31-03 

11. Contract or Grant No. 

NAS1-18226 

13. Type of Report and Period Covered 

Contractor Report 

14. Sponsoring Agency Code 

Technical Monitor: 

Task 5 Final Report 

Sally C. Johnson, Langley Research Center 

6. Abstract 

The application of formal verification techniques to AI software, particularly 

expert systems, is investigated. Constraint satisfaction and model inversion 

are identified as two formal specification paradigms for different classes of 

expert systems. 

of approximate semantics is introduced. 

can be applied in both declarative and imperative forms. 

A formal definition of consistency is developed, and the notion 

Examples are given of how-these ideas 

7. Key Words (Suggested by Author(s)) I 18. Distribution Statement 

Formal Verification 

Artificial Intelligence 

1 Unclassified-Unlimi ted 

Unclassified I Unclassified 1 158 I I I 

4SA FORM lG!6 OCT 86