Kowalski, R.



A logic-based calculus of events

Classics

We outline an approach for reasoning about events and time within a logic programming framework. The notion of event is taken to be more primitive than that of time and both are represented explicitly by means of Horn clauses augmented with negation by failure. Default reasoning on the basis of incomplete information is obtained as a consequence of using negation by failure. Because events are differentiated from times, we can represent events with unknown times, as well as events which are partially ordered and concurrent.


Predicate logic as a programming language

Classics

"Sentences in first-order predicate logic can be usefully interpreted as programs. In this paper the operational and fixpoint semantics of predicate logic programs are defined, and the connections with the proof theory and model theory of logic are investigated. It is concluded that operational semantics is a part of proof theory and that fixpoint semantics is a special case of model-theoretic semantics."From: M. H. Van Emden and R. A. Kowalski. The Semantics of Predicate Logic as a Programming Language. Journal of the ACM (JACM) JACM Homepage archive. Volume 23 Issue 4, Oct. 1976, Pages 733-742IFIP 74. Amsterdam: North-Holland, 569-574.


And-or graphs, theorem-proving graphs, and bi-directional search

Classics

And-or graphs and theorem-proving graphs determine the same kind of search space and differ only in the direction of search: from axioms to goals, in the case of theorem-proving graphs, and in the opposite direction, from goals to axioms, in the case of and-or graphs. We investigate the construction of a single general algorithm which covers unidirectional search both for and-or graphs and for theorem-proving graphs, bidirectional search for path-finding problems and search for a simplest solution as well as search for any solution. Indeed, many different search spaces can represent the same original problem, as in the case of resolution systems where different refinements of the resolution rule determine different search spaces for a single problem of demonstrating the unsatisfiability of a given set of clauses. In the tree representation of theorem-proving graphs (used in Machine Intelligence 5 (Kowalski 1969)), identical problems Tare generated at different times, working forwards from the initial set of axioms {D, E, F, G}.