Logic and Knowledge Representation

Home

My research uses cut-free sequent calculi to study such logical search problems. Cut-free sequent calculi describe how proofs can be constructed by decomposing the formulas that represent premises or conclusions of the proof according to the meanings of their logical connectives. Sequent calculi can differ, among other things, in the bookkeeping regimes they use to keep track of dependencies in the proof (such as constraints on the values of variables or constraints on the uses of premises). Some regimes are suited to the use of proofs (for example to specify algorithms or to report reasoning to people); these regimes tend to build dependencies into the structure of proofs. Others regimes are suited to search for proofs; these tend to factor dependencies into independent representations that are built monotonically as a proof is constructed.

Syntactic transformations between proofs in different systems therefore become important:

• to design calculi that describe effective search for theorem-proving or logic programming applications and that provably correspond to simple or canonical calculi;
• to enable proofs found by efficient methods to be used for new purposes;
• to study the results that can be proved and the representations that are needed for specialized theorem-proving problems.

My research has been exploring a representation of plans as proofs in a logical theory of action, time and knowledge. This view not only allows plans to be constructed by logical proof-search techniques, but also allows plans to be transformed and reused respecting proof-theoretic principles. We therefore find a systematic application of the full range of techniques in computational logic. The main challenge of this perspective is to find proof problems that are faithful to the context of an agent's deliberation and action and that afford specialized search techniques of the sort developed in implemented planners. Preliminary results, implemented in the context of collaborative dialogue agents, provide good reason to be optimistic on this front.

Pure Logic

Dissertation	Matthew Stone. Modality in Dialogue: Planning, Pragmatics and Computation. PhD Thesis, Department of Computer and Information Science, University of Pennsylvania, 1998. My dissertation is devoted to the proof-theoretic development of a logic programming language based on modal logic and the application of modal logic programming to reasoning about knowledge and action in planning and in natural language generation. Many of the papers that follow appear here as chapters. The dissertation is also available from Penn as IRCS report 98-23.
Stone 99	Matthew Stone. Representing Scope in Intuitionistic Deductions. Theoretical Computer Science 211(1-2), 1999, pages 129--188. This paper uses permutation of inference to establish relationships among a number of proof systems for intuitionistic logic; the result has applications in theorem-proving, logic programming and program synthesis. The electronic version available here is the Penn Tech Report. The final version (for copyright reasons) is instead available from the publisher to subscribers to TCS.
Stone, to appear	Matthew Stone. Disjunction and Modular Goal-directed Proof Search. This paper explores goal-directed proof search in first-order multi-modal logic. The key issue is to design a proof system that respects the modularity and locality of assumptions of many modal logics. By forcing ambiguities to be considered independently, modular disjunctions in particular can be used to construct efficiently executable specifications in reasoning tasks involving partial information that otherwise might require prohibitive search. Distributed on arxiv.org, 2002. Comments welcome and appreciated. Substantially replaces Indefinite information in modal logic programming. Matthew Stone. RuCCS TR 56, 1999. Complements First-order multi-modal deduction. Matthew Stone. RuCCS TR 55, 1999. This paper explores prefixed tableaux for first-order multi-modal logic, providing proofs for soundness and completeness theorems, a Herbrand theorem on deductions describing the use of Herbrand or Skolem terms in place of parameters in proofs, and a lifting theorem describing the use of variables and constraints to describe instantiation. Complements Efficient tree construction for reasoning about necessity. Matthew Stone. Distributed as IRCS TR 97-07, University of Pennsylvania, 1997. This paper develops polynomial-time constraint algorithms that can be used to solve certain equational unification problems required to identify possible worlds in modal proofs, under the so-called functional translation of modal logic into classical logic.

Logic in Artificial Intelligence

Stone 02	Matthew Stone. Knowledge Representation. A practical survey of the knowledge representation required for deep natural language processing systems. A revised version of this manuscript will appear in Farghaly, ed., A Handbook for Language Engineers, to be published by CSLI, 2002. Comments welcome and appreciated.
Stone 01	Matthew Stone. Representing Communicative Intentions in Collaborative Conversational Agents. AAAI Fall Symposium on Intent Inference for Collaborative Tasks, November 2001. The contribution of this paper is a general representation of collaborative plans and intentions, inspired by representations of deductions in logics of knowledge, action and time, which supports agents in coordinating abstractly about future decisions when agents have access to different information.
Stone 98	Matthew Stone. Abductive Planning with Sensing. AAAI 1998, pages 631--636. This paper shows how planning in the context of partial information can be cast as a theorem-proving problem to be solved by abductive inference: the conjecture to be proved is that the goal knowably holds true after a series of steps of deliberation and action; the assumptions that can be made consider the known consequences of an action that could be concretely chosen by the agent at some stage of the plan.
Stone 97b	Matthew Stone. Partial-order Reasoning for a Nonmonotonic Logic of Action. AAAI 1997 Workshop on Robots, Softbots and Immobots. This paper applies constraint algorithms for modal prefix unification to the case where modal operators describe temporal change. Factoring inertial reasoning into modal prefixes using argumentation leads to the kind of partial-order reasoning used in implemented planners.
Stone 97c	Matthew Stone. Applying Theories of Communicative Action in Generation Using Logic Programming. AAAI 1997 Fall Symposium On Communicative Action in Humans and Machines. This paper describes the use of modal logic and modal logic programming (including constraint reasoning about possible worlds) to represent the knowledge of participants in conversation and the evolution of that knowledge during dialogue.