Contents
Computational Logic
Plan Representation
Publications
Links
Home

Computational Logic
Logic is broadly concerned with studying inference and expressive
power of formal languages with welldefined meanings. Computational
logic emphasizes the design of finite inference procedures and
analysis of complexity and proof search in them.
My research uses cutfree sequent calculi to study such logical
search problems. Cutfree 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
theoremproving 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 theoremproving
problems.
I have been studying these questions with particular attention
to modal and intuitionistic logics, because of these logics' close
connection with the planning and commonsense reasoning problems faced
by collaborative systems and conversational agents.
Plan Representation
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 proofsearch
techniques, but also allows plans to be transformed and reused
respecting prooftheoretic 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.
Publications
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 prooftheoretic
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 9823.

Stone 99

Matthew Stone. Representing Scope in Intuitionistic Deductions.
Theoretical Computer Science 211(12), 1999, pages 129188.
This paper uses permutation of inference to establish relationships
among a number of proof systems for intuitionistic logic; the result
has applications in theoremproving, 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 Goaldirected Proof
Search.
This paper explores goaldirected proof search in firstorder
multimodal 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 Firstorder multimodal
deduction. Matthew Stone. RuCCS TR 55, 1999.
This paper explores prefixed tableaux for firstorder multimodal 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
9707, University of Pennsylvania, 1997.
This paper develops polynomialtime constraint algorithms that can
be used to solve certain equational unification problems required
to identify possible worlds in modal proofs, under the socalled
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 631636.
This paper shows how planning in the context of partial information
can be cast as a theoremproving 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.
Partialorder 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 partialorder 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.

Links
