[Prev][Next][Index][Thread]
Logic/Semantics Tools from Kansas State University

To: types@dcs.gla.ac.uk

Subject: Logic/Semantics Tools from Kansas State University

From: Allen Stoughton <allen@cis.ksu.edu>

Date: Tue, 6 Aug 1996 14:28:00 0500 (CDT)

Approved: types@dcs.gla.ac.uk
[ The Types Forum  http://www.dcs.gla.ac.uk/~types ]
Logic/Semantics Tools from Kansas State University
******************************************************************************
Version 1.0 of Porgi, a ProofOrRefutation 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, treebased 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 obtainedin both source and binary (SPARC/Solaris)
formsvia 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