Consider the predicate logic language with three constants Mike, Bi ll and John,

Question

Consider the predicate logic language with three constants Mike, Bi ll and John, and three rel at ions Hits(x, y), Tall (x), and Alive(x). I show the var iables after the relat ion name just to indicate how many arguments the relat ion expects M1. Show a predicate logic model for this language M2. How many predicate logic mode ls are there for this language? M3. How many predicate logic mode ls are there for this language if you consider only the domain 1 ( a. Does {P entaiQ If not, show a predicate logic model that is M4. Let P be the formula Hits (Mike, John) and Q be the formula forall x) ( forall y) Hits(x, y) a counter example. If so, expand the def inition of "entails" to say what "P entailsQ means without using the word "ent ai Is" b. Does Q ent ail P If not, show a predicate logic model that is a counter example. If so, expand the def inition of "entails" to say what entails P" means without using the word "ent ai Is

Explanation / Answer

Predicate logic plays an important role m many formal models of computer programs [3,
14, 17]. Here we are concerned with the interpretation of predicate logic as a program-
ming language [5, 10]. The PROLOG system (for PROgramming in LOGic), based upon
the procedural interpretation, has been used for several ambitious programming tasks
(including French language question answermg ]5, 18], symbolic mtegration [9], plan
formation [24], theorem provmg, speech recognmon, and picture interpretation). In this
paper we ignore the practical aspects of programming m logic and investigate instead the
semantics of predicate logic regarded as a programming language. We compare the
resulting semantics with the classical semantics studied by logicians.
Two kinds of semantics [22], operational and fixpomt, have been defined for program-
mmg languages. Operational semantics defines the input-output relation computed by a
program m terms of the mdivldual operations evoked by the program inside a machine.
The meaning of a program ts the mput-output relation obtained by executing the
program on the machine. As a machine independent alternative to operational seman-
tics, fixpoint semantics [1,6, 17, 22] defines the meamng of a program to be the input-
output relation which ts the mimmal fixpoint of a transformation assooated with the
program. Fixpomt semantics has been used [6, 7, 15, 17] to justify existing methods for
proving properties of programs and to motivate and justify new methods of proof.
Logicians &stinguish between the syntax and the semantics of formal languages.
Syntax deals with the formal part of language m abstraction from its meaning. It deals
not only with the definition of well-formed formulas, syntax in its narrow sense, but also
w~th the broader study of axioms, rules of reference, and proofs, which constitutes proof
theory. Semantics, on the other hand, deals with the interpretation of language and
includes such notions as meaning, logical implication, and truth. Church's Introduction to
Mathematical Logic [4] contains a thorough discussion of the respectwe roles of syntax
and semantics.
Copyright © 1976, Association for Computing Machinery, Inc General permission to republish, but not for
profit, all or part of this material ~s granted provided that ACM's copyright notice is given and that reference is
made to the publication, to its date of ~ssue. and to the fact that reprinting prlvdeges were granted by
permlss~on of the Association for Computing Machinery
This work was supported by the U K Science Research Council
Authors" present addresses M H van Emden, Department of Computer Science, Umvers~ty of Waterloo,
Waterloo, Ontario, Canada N2L 3G1, R A Kowalskl, Department of Computation & Control, Imperial
College, 180 Queens Gate. London SW7, Umted Kingdom
We use the interpretation of predicate logic as a programming language in order to
compare the notions of operational and fixpomt semantics of programming languages
with the notions of syntax and semantics of predicate logic. We show that operational
semantics is included in the part of syntax concerned with proof theory and that fixpomt
semantics ~s a specml case of model-theoretic semantics. With this interpretation of
operational semantics as syntax and fixpoint semanncs as semantics, the eqmvalence of
operational and fixpoint semantics becomes a special case of Godel's completeness
theorem.
This paper is concerned with the analysis and comparison of some of the most basic
notions of logic and computatmn As a by-product it is virtually self-contained and
requires only a general knowledge of logic but no special famiharity with the operational
and fixpoint semantics of programming languages.
2. A Syntax of Well-Formed Formulas
It is convement to restrict attention to predicate logic programs written m clausal form.
Such programs have an especially simple syntax but retain all the expressive power of the
full predicate logic.
A sentence Is a finite set of clauses.
A clause is a disjunction Li V " • • V Ln of literals L,, which are atomtc formulas
P(tl, . . . , tin) or the negations of atomic formulas P(tl ..... tin), where P is a predicate
symbol and t, are terms. Atomic formulas are positive literals. Negatmns of atomic
formulas are negative literals.
A term is either a variable or an expression f(tl ..... tin) where f is a function symbol
and t, are terms. Constants are 0-ary function symbols.
A set of clauses {C1 .... , C,,} is interpreted as the conjunction, C1 and.., and Cn. A
clause C containing just the vanablesx~,..., xm Is regarded as universally quantified:
for all x~, . .., x,n C
For every sentence S~ m predicate logm there exists a sentence Sz in clausal form which is
satisfiable ff and only ff S~ is. For this reason, all questmns concerning the validity or
satisfmbility of sentences m predmate logm can be addressed to sentences m clausal form.
Methods for transforming sentences into clausal form are described m [16].
We have defined that part of the syntax of predmate loDc which is concerned with the
specification of well-formed formulas. Aspects of syntax concerned with proof theory are
dealt with m the next two sections.
3. The Procedural lnterpretauon
It is easiest to interpret procedurally sets of clauses which contain at most one posmve
hteral per clause. Such sets of clauses are called Horn sentences. We distinguish three
kinds of Horn clauses.
(1) [] the empty clause, containing no hterals and denoting the truth value false, is
interpreted as a halt statement.
(2) B~ V • • • V Bn a clause consisting of no positive hterals and n -> 1 negative hterals
~s interpreted as a goal statement.
(3) A V B1 V • - • V B,, a clause consisting of exactly one positive hteral and n >- 0
negatwe literals ~s interpreted as a procedure declaration. The posmve hteral A is the
procedure name and the negative literals are the procedure body. Each negative
literal B, in the procedure body is interpreted as a procedure call. When n = 0 the
procedure declaratmn has an empty body and ~s interpreted as an unquahfied
assertion of fact
In the procedural mterpretatmn a set of procedure declaratmns ~s a program. Compu-
tatmn ~s inmated by an mitml goal statement, proceeds by using procedure declaratmns
The Semanttcs of Predtcate Logtc as a Programmtng Language 735
to derive new goal statements from old goal statements, and terminates with the
derivation of the halt statement Such derivanon of goal statements is accomplished by
resolution [20], which is interpreted as procedure invocatton. Gwen a selected procedure
call A, reside the body of a goal statement
A~ V "" VA,_~ V,a., VA,+l V "'" V-4n
and given a procedure declaranon
A'VB~V... VB,,, m>-O
whose name matches the selected procedure call (m the sense that some most general
substitution 0 of terms for variables makes A, and A' identical), resolution derives the
new goal statement
(A,V ... VA,_, V B, V ... V/~m VA,+, V """ VA,)O.
In general, any derivation can be regarded as a computation and any refutation (i.e.
derivation of D) can be regarded as a successfully terminating computation. However
only goal oriented resolution derivations correspond to the standard notion of computa-
tion. Such a goal-orwnted denvatton from an initial set of Horn clauses A and from an
mitml goal statement C~ in A ~s a sequence of goal statements C1, • •., Cn such that each
C, contains a single selected procedure call and C,+1 is obtained from C, by procedure
mvocat~on relatwe to the selected procedure call in C, using a procedure declaration m
A
In model ehmlnatlon [131, ordered linear resolution [19], and SL-resolutlon [12], the
selection of procedure calls ~s governed by the last m/first out rule: A goal statement is
treated as a stack of procedure calls. The selected procedure call must be at the top of the
stack. The new procedure calls which by procedure lnvocanon replace the selected
procedure call are inserted at the top of the stack. The more general notion of goal
oriented derivation defined above corresponds to computation with coroutines [10].
Computation with asynchronous parallel processes is obtained by using the sphttmg rule
[2, 8, 231.
Pre&cate logic is a nondetermmistic programming language: Given a single goal
statement, several procedure declarations can have a name which matches the selected
procedure call. Each declaratton gwes rise to a new goal statement. A proof procedure
which sequences the generanon of derivations m the search for a refutation behaves as an
mterpreter for the program incorporated in the initml set of clauses. These and other
aspects of the procedural interpretation of Horn clauses are investigated m greater detad
elsewhere [10]
The procedural interpretation has also been investigated for non-Horn clauses [11].
However, m this paper we restrict ourselves to Horn clauses.
Example The following two clauses constitute a program for appending two lists.
The term cons(x,y) is interpreted as a list whose first element, the head, Is x and whose
tad, y, ~s the rest of the list. The constant nil denotes the empty list. The terms u, x, y,
and z are varmbles. Append(x,y,z) denotes the relationship: Z is obtained by appending
y tox.
(1) Appen(nd,x,x).
(2) Append(cons(x,y)~z,cons(x,u))V Append(y,z,u)
To compute the result of appending the list cons(b,nil) to the list cons(a,nil), the
program is actwated by the goal statement
(3) App~(cons( a ,nll ),cons( b ,nil),v ),
where v is a varmble and a and b are constants, the "atoms" of the hsts With this goal
statement the program is deterministic. With a goal directed theorem prover as inter-
preter, the following computation ensues:
C1 = Append(cons(a,nil),cons(b,ml),v),
C~ = App-~d(nil,cons(b,nil),w) 01,
C3 = E/0z,

Related Questions

Navigate

• Browse (All)
• Browse C
• Subjects

---

---

Integrity-first tutoring: explanations and feedback only — we do not complete graded work. Learn more.