A wide range of problems, from contingent and multiagent planning to process/service orchestration, can be viewed as games. In many of these, it is natural to spec- ify the possible behaviors procedurally. In this paper, we develop a logical framework for specifying these types of problems/games based on the situation calculus and ConGolog. The framework incorporates game-theoretic path quantifiers as in ATL. We show that the framework can be used to model such problems in a natural way. We also show how verification/synthesis techniques can be used to solve problems expressed in the framework. In particular, we develop a method for dealing with infinite state settings using fixpoint approximation and “characteristic graphs”.

A plan with rich control structures like branches and loops can usually serve as a general solution that solves multiple planning instances in a domain. However, the correctness of such generalized plans is non-trivial to define and verify, especially when it comes to whether or not a plan works for all of the infinitely many instances of the problem. In this paper, we give a precise definition of a generalized plan representation called an FSA plan, with its semantics defined in the situation calculus. Based on this, we identify a class of infinite planning problems, which we call one-dimensional (1d), and prove a correctness result that 1d problems can be verified by finite means. We show that this theoretical result leads to a practical algorithm that does this verification practically, and a planner based on this verification algorithm efficiently generates provably correct plans for 1d problems.

Dynamic epistemic logic deals with the representation of situations in a multi-agent and dynamic setting. It allows to express in a uniform way statements about: 1. what is true about an initial situation 2. what is true about an event occurring in this situation 3. what is true about the resulting situation after the event has occurred. We axiomatize in this framework what we can infer about (3) given (1) and (2), introducing thereby new techniques to prove completeness. We also show that this axiomatization is decidable. Besides being useful for reasoning about actions, it provides a natural characterization of the product update of dynamic epistemic logic.

This paper constructively proves the existence of an effective procedure generating a computable (total) function that is not contained in any given effectively enumerable set of such functions. The proof implies the existence of machines that process informal concepts such as computable (total) functions beyond the limits of any given Turing machine or formal system, that is, these machines can, in a certain sense, "compute" function values beyond these limits. We call these machines creative. We argue that any "intelligent" machine should be capable of processing informal concepts such as computable (total) functions, that is, it should be creative. Finally, we introduce hypotheses on creative machines which were developed on the basis of theoretical investigations and experiments with computer programs. The hypotheses say that machine intelligence is the execution of a self-developing procedure starting from any universal programming language and any input.

Electronic Geometry Textbook is a knowledge management system that manages geometric textbook knowledge to enable users to construct and share dynamic geometry textbooks interactively and efficiently. Based on a knowledge base organizing and storing the knowledge represented in specific languages, the system implements interfaces for maintaining the data representing that knowledge as well as relations among those data, for automatically generating readable documents for viewing or printing, and for automatically discovering the relations among knowledge data. An interface has been developed for users to create geometry textbooks with automatic checking, in real time, of the consistency of the structure of each resulting textbook. By integrating an external geometric theorem prover and an external dynamic geometry software package, the system offers the facilities for automatically proving theorems and generating dynamic figures in the created textbooks. This paper provides a comprehensive account of the current version of Electronic Geometry Textbook.

Computability logic (CL) (see http://www.cis.upenn.edu/~giorgi/cl.html ) is a research program for redeveloping logic as a formal theory of computability, as opposed to the formal theory of truth which it has more traditionally been. Formulas in CL stand for interactive computational problems, seen as games between a machine and its environment; logical operators represent operations on such entities; and "truth" is understood as existence of an effective solution. The formalism of CL is open-ended, and may undergo series of extensions as the studies of the subject advance. So far three -- parallel, sequential and choice -- sorts of conjunction and disjunction have been studied. The present paper adds one more natural kind to this collection, termed toggling. The toggling operations can be characterized as lenient versions of choice operations where choices are retractable, being allowed to be reconsidered any finite number of times. This way, they model trial-and-error style decision steps in interactive computation. The main technical result of this paper is constructing a sound and complete axiomatization for the propositional fragment of computability logic whose vocabulary, together with negation, includes all four -- parallel, toggling, sequential and choice -- kinds of conjunction and disjunction. Along with toggling conjunction and disjunction, the paper also introduces the toggling versions of quantifiers and recurrence operations.

Simple type theory is suited as framework for combining classical and non-classical logics. This claim is based on the observation that various prominent logics, including (quantified) multimodal logics and intuitionistic logics, can be elegantly embedded in simple type theory. Furthermore, simple type theory is sufficiently expressive to model combinations of embedded logics and it has a well understood semantics. Off-the-shelf reasoning systems for simple type theory exist that can be uniformly employed for reasoning within and about combinations of logics.

We present DCL-PC: a logic for reasoning about how the abilities of agents and coalitions of agents are altered by transferring control from one agent to another. The logical foundation of DCL-PC is CL-PC, a logic for reasoning about cooperation in which the abilities of agents and coalitions of agents stem from a distribution of atomic Boolean variables to individual agents -- the choices available to a coalition correspond to assignments to the variables the coalition controls. The basic modal constructs of DCL-PC are of the form `coalition C can cooperate to bring about phi'. DCL-PC extends CL-PC with dynamic logic modalities in which atomic programs are of the form `agent i gives control of variable p to agent j'; as usual in dynamic logic, these atomic programs may be combined using sequence, iteration, choice, and test operators to form complex programs. By combining such dynamic transfer programs with cooperation modalities, it becomes possible to reason about how the power of agents and coalitions is affected by the transfer of control. We give two alternative semantics for the logic: a `direct' semantics, in which we capture the distributions of Boolean variables to agents; and a more conventional Kripke semantics. We prove that these semantics are equivalent, and then present an axiomatization for the logic. We investigate the computational complexity of model checking and satisfiability for DCL-PC, and show that both problems are PSPACE-complete (and hence no worse than the underlying logic CL-PC). Finally, we investigate the characterisation of control in DCL-PC. We distinguish between first-order control -- the ability of an agent or coalition to control some state of affairs through the assignment of values to the variables under the control of the agent or coalition -- and second-order control -- the ability of an agent to exert control over the control that other agents have by transferring variables to other agents. We give a logical characterisation of second-order control.

Research effort, with its emphasis on evaluation and measurable progress, things began to change. Instead SHRDLU (WIN72) is perhaps the canonical example. of systems whose architecture and vocabulary were The rapid growth of efforts to found the next generation of based on linguistic theory (in this case acoustic phonetics), systems on general-purpose knowledge representation languages new approaches based on statistical modelling and Bayesian (I'm thinking of several varieties of semantic nets, probability emerged and quickly spread. "Every time I fire a from plain to partitioned, as well as KRL, KL-ONE and linguist my system's performance improves" (Fred Jellinek, their successors, ending (not yet, of course) with CYC (See head of speech recognition at IBM, c. 1980, latterly repudiated (BRA08) for all these) stumbled to a halt once their failure by Fred but widely attested). As advanced from resolution theorem provers through a number more and more problems are re-conceived as instances of of stages to the current proliferation of a range of Description the noisy channel model, the empiricist paradigm continually Logic'reasoners'; Whereas in the 1970s and 1980s there grew, so did the need to manage the impact of change and was real energy and optimism at the interface between computational conflict: enter'truth maintenance', subsequently renamed and theoretical linguistics, the overwhelming success'reason maintenance'. While still using some of But outflanking these'normal science' advances of AI, the terminology of linguistic theory, computational linguistics the paradigm shifters were coming up fast on the outside: practioners are increasingly detached from theory itself, over the last ten years machine learning has spread from which has suffered a, perhaps connected, loss of energy and small specialist niches such as speech recognition to become sense of progress.

In this paper we address an issue that has been brought to the attention of the database community with the advent of the Semantic Web, i.e. the issue of how ontologies (and semantics conveyed by them) can help solving typical database problems, through a better understanding of KR aspects related to databases. In particular, we investigate this issue from the ILP perspective by considering two database problems, (i) the definition of views and (ii) the definition of constraints, for a database whose schema is represented also by means of an ontology. Both can be reformulated as ILP problems and can benefit from the expressive and deductive power of the KR framework DL+log. We illustrate the application scenarios by means of examples. Keywords: Inductive Logic Programming, Relational Databases, Ontologies, Description Logics, Hybrid Knowledge Representation and Reasoning Systems. Note: To appear in Theory and Practice of Logic Programming (TPLP).