[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.