We consider a class of knowledge-based Golog programs with sense actions. These programs refer explicitly to an agent's knowledge, and are designed to execute on-line, and under a dynamic closed-world assumption on knowledge. On-line execution of sense actions dynamically updates the background axioms with sentences asserting knowledge of the sense actions' outcomes. We formalize what all this might mean, and show that under suitable assumptions the knowledge modality in such programs can be implemented by provability. This leads to an on-line Golog interpreter for such programs, which we demonstrate on a knowledge-based program with sensing for the blocks world.

We focus on a rich axiomatization for actions in the situation calculus that includes, among other features, a solution to the frame problem for deterministic actions. Our work is foundational in nature, directed at simplifying the entailment problem for these axioms. Specifically, we make four contributions to the metatheory of situation calculus axiomatizations of dynamical systems: (1) We prove that the above-mentioned axiomatization for actions has a relative satisfiability property; the full axiomatization is satisfiable iff the axioms for the initial state are. (2)We define the concept of regression relative to these axioms, and prove a soundness and completeness theorem for a regression-based approach to the entailment problem for a wide class of queries. (3) Our formalization of the situation calculus requires certain foundational axioms specifying the domain of situations. These include an induction axiom, whose presence complicates human and automated reasoning in the situation calculus. We characterize various classes of sentences whose proofs do not require induction, and in some cases, some of the other foundational axioms. (4)We prove that the logic programming language GOLOG never requires any of the foundational axioms for the evaluation of programs.

The paper provides examples of situations where formal specifications of procedures in the standard pre/postcondition style become lengthy, cumbersome and difficult to change, a problem which is particularly acute in the case of object oriented specifications with inheritance. We identify the problem as the inability to express that a procedure changes only those things it has to, leaving everything else unmodified, and review some attempts at dealing with this "frame problem" in the software specification community. The second part of the paper adapts a recent proposal for a solution to the frame problem in artificial intelligence-the notion of explanation closure axioms-to provide an approach whereby one can state such conditions succinctly and modularly, with the added advantage of having the specifier be reminded of things that she may have omitted saying in procedure specifications. Since this approach is based on standard predicate logic, its semantics are relatively straightforward. The paper also suggests an algorithm which generates syntactically the explanation closure axioms from the pre/postcondition specifications, provided they are written in a restricted language; it also suggests a model theory supporting it.>

We investigate the possibility of using circumscription for characterizing the concept of a generic object in the context of a formalized mathematical theory. We show that conventional circumscriptive policies do not give the intuitively expected res

We pursue the perspective of Reiter that in situation calculus one can formalize primitive, determinate actions with axioms which, among others, include two disjoint sets: a set of successor state axioms and a set of action precondition axioms. We posed ourselves the problem of automatically generating successor state axioms, given only a set of effect axioms and a set of state constraints. This is a special version of what has been traditionally called the ramification problem. To our surprise, we found that there are state constraints whose role is not to yield indirect effects of actions. Rather, they are implicit axioms about action preconditions. As such, they are intimately related to the classical qualification problem. We also discovered that other kinds of state constraints arise; these are related to the formalization of strategic or control information. This paper is devoted to describing our results along these lines, focusing on ramification and qualification state constraints. More specifically, we propose a two-step procedure for determining an axiomatization which monotonically solves our versions of the ramification and qualification problems. We justify the first step semantically by appealing to a suitable minimization policy. Step two we justify by simple Clark predicate completion.

A sound and, in certain cases, complete method is described for evaluating queries in relational databases with null values where these nulls represent existing but unknown individuals. The soundness and completeness results are proved relative to a formalization of such databases as suitable theories of first-order logic. Because the algorithm conforms to the relational algebra, it may easily be incorporated into existing relational systems.

We focus on McCarthy's method of predicate circumscription in order to establish various results about its consistency, and about its ability to conjecture new information. A basic result is that predicate circumscription cannot account for the standard kinds of default reasoning. Another is that predicate circumscription yields no new information about the equality predicate. This has important consequences for the unique names and domain closure assumptions.

A class of first-order databases with no function signs is considered. A closed database DB is one for which the only existing individuals are those explicitly referred to in the formulas of DB. Formally, this is expressed by including in DB a domain closure axiom ( x ) x = c 1 ∨···∨ x = c p , where c 1 ,…, c p are all of the constants occurring in DB. It is shown how to completely capture the effects of this axiom by means of suitable generalizations of the projection and division operators of relational algebra, thereby permitting the underlying theorem prover used for query evaluation to ignore this axiom. A database is E-saturated if all of its constants denote distinct individuals. It is shown that such databases circumvent the usual problems associated with equality, which arise in more general databases. Finally, it is proved for Horn databases and positive queries that only definite answers are obtained, and for databases with infinitely many constants that infinitely long indefinite answers can arise.

A semantic and deductive formal system for automatic theorem proving is presented. The system has, as its deductive component, a form of natural deduction. Its semantic component relies on an underlying representation of a model. This model is invoked to prune subgoals generated by the deductive component, whenever such subgoals test false in the model. In addition, the model is used to suggest inferences to be made at the deductive level. Conversely, the current state of the proof suggests changes to be made to the model, e.g., when a construction is required as in geometry.

Resolution with merging, linear format, and set of support is shown to be compatible with an A-ordering restriction; in any resolution operation under a linear format, the literal resolved upon in the near parent must be a maximal literal in that clause.The far parent must either be a merge, in which case the literal resolved upon must be a merge literal, or a member of the original set of clauses.A new kind of ordering, called C-ordering, is introduced and shown to be compatible with merge, linear format, and set of support resolution.Its advantage over A-ordering is that the literal to be resolved upon in the near parent is uniquely specified.

The predicate elimination strategy is a complete resolution proof strategy for multi-predicate formulas. Essentially, the procedure focuses on one of the predicate symbols P, and attempts to deduce clauses independent of P by means of resolution in which only predicates in P are “resolved away” from parent clauses. The completeness theorem states that one can in this way, deduce an unsatisfiable P-independent set of clauses, provided the given set is unsatisfiable.

A model for parallel computations is given as a directed graph in which nodes represent elementary operations, and branches, data channels. The problem considered is the determination of an admissible schedule for such a computation; i.e. for each node determine a sequence of times at which the node initiates its operation. These times must be such that each node, upon initiation, is assured of having the necessary data upon which to operate. Necessary and sufficient conditions that a schedule be admissible are given. The computation rate of a given admissible schedule is defined and is shown to have a limiting value 1/π where π is a parameter dependent upon the cycles in the graph. Thus, the computation cannot proceed at a rate exceeding 1/π. For γ ≥ π, the class of all periodic admissible schedules with period γ is characterized by the solution space of a certain system of linear inequalities. In particular, then, the maximum computation rate of 1/π is attainable under a periodic admissible schedule with period π. A class of all-integer admissible schedules is given. Finally, an algorithm is given for the determination of the number of initiations of each node in the graph defining a parallel computation. An example for a system of difference equations is given in detail.