[Prev][Next][Index][Thread]
definitions in sequent calculus
A notion of definition has been introduced in sequent calculus
in recent years by, for example, Eriksson, Girard, Hallnas,
Schroeder-Heister, and Staerk. Definitions extend theories in the
sense that while they both provide formulas for constructing
proofs, definitions carry the added intension that there are no
other ways that defined concepts can be proved. The use of
definitions captures some aspects of the closed world assumption.
Definitions can be added to sequent systems via the addition
of a left- and a right-introduction rule.
The following three papers explore the use of definitions in the
specification and reasoning about computations. These papers can
be found either at
ftp://ftp.cis.upenn.edu/pub/papers/miller/ or
http://hypatia.dcs.qmw.ac.uk/authors/M/MillerD/.
Cut Elimination for a Logic with Definitions and Induction, by
Raymond McDowell and Dale Miller. Submitted to the Proceedings
of the TYPES'96 Workshop. Available as cut_elim.dvi.gz and
cut_elim.ps.gz.
This paper proves that sequent calculus for intuitionistic
logic extended with definitions and natural number induction
satisfies cut-elimination. Definitions may have implications
in their bodies if they are suitably "stratified".
Encoding Transition Systems in Sequent Calculus, by Raymond
McDowell, Dale Miller, and Catuscia Palamidessi. Submitted to
Theoretical Computer Science. Available as tcs97.dvi.gz and
tcs97.ps.gz.
While traditional sequent calculi can generally capture MAY
behavior of computations, this paper shows how definitions can
be used to capture MUST behavior. This is illustrated using
simulation and bisimulation. Induction is also used to
prove properties about some infinite computation.
A Logic for Reasoning with Higher-Order Abstract Syntax, by
Raymond McDowell and Dale Miller. To appear in LICS'97, Warsaw.
Available as lics97.ps.gz.
Definitions can be used to reason about computations that have been
specified in logical frameworks. Definitions can be used at
one level to reason about how proofs of an object-level
statement must have been constructed. Thus it is possible,
for example, to provide formal, sequent calculus proofs of
meta-level statements such as subject-reduction and determinacy
of evaluation.
----------------------------------------------------------------
Please address administrative mail regarding the lambda Prolog mailing list to
lprolog-request@cis.upenn.edu. See http://www.cis.upenn.edu/~dale/lProlog.