[Prev][Next][Index][Thread]

Logic/Semantics Tools from Kansas State University


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

          Logic/Semantics Tools from Kansas State University

******************************************************************************

Version 1.0 of Porgi, a Proof-Or-Refutation Generator for
Intuitionistic propositional logic, is now available.

Given a sequent Gamma |- phi, Porgi either finds a minimally sized,
normal natural deduction of phi from the assumptions in Gamma, or it
finds a finite, tree-based Kripke model whose root node forces all of
the formulas in Gamma but does not force phi.  Although an attempt is
made to minimize the size of the Kripke countermodels, such
countermodels are not always minimally sized.  On the other hand:

  (a) Classical models are produced whenever possible.  Thus, if a
      model with more than one node is produced, one can conclude that
      the sequent is provable classically.

  (b) In Porgi's countermodels, child nodes always force strictly more
      subformulas of the formulas of the sequent than do their parents.

  (c) In one of Porgi's countermodels, all nodes other than the root
      node force the formula phi.

Porgi can also handle minimal logic, is capable of generating typed
lambda terms instead of natural deductions, and can display the
subformulas of a sequent that are forced at each node of a Kripke
countermodel.

Porgi is implemented in Standard ML (SML/NJ Version 0.93), but
produces a UNIX command, which can be invoked from the shell.  Porgi
can be obtained---in both source and binary (SPARC/Solaris)
forms---via WWW URL

  http://www.cis.ksu.edu/~allen/porgi.html

******************************************************************************

Lambda, a program for solving lambda definability problems of order at
most two, is still available (now also in SPARC/Solaris binary form)
via WWW URL

  http://www.cis.ksu.edu/~allen/lambda.html

******************************************************************************

Allen Stoughton
allen@cis.ksu.edu
http://www.cis.ksu.edu/~allen/home.html