Logic is broadly concerned with studying inference and expressive
power of formal languages with well-defined meanings. Computational
logic emphasizes the design of finite inference procedures and
analysis of complexity and proof search in them.
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:
I have been studying these questions with particular attention
to modal and intuitionistic logics, because of these logics' close
connection with the planning and common-sense reasoning problems faced
by collaborative systems and conversational agents.
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
to study the results that can be proved and the
representations that are needed for specialized theorem-proving
As a representation, a plan guides the deliberation and action of an
agent by describing the consequences (generally favorable) of a series
of actions that the agent can feasibly choose and carry out. Such
plans have a variety of uses: agents need them to collaborate with
other agents, to respond to changing goals and circumstances, and to
narrow its deliberation based on its existing commitments. Plans are
more than programs that an agent cooks up, blindly runs, and discards.
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.
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
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
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
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
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
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
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.
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.
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.
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.
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.