@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
Name: Porgi
Keywords: intuitionistic, propositional, natural deduction, Kripke model
Description:
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.
Contact persons: Allen Stoughton allen@cis.ksu.edu
Documentation:
See WWW URL http://www.cis.ksu.edu/~allen/porgi.html. Porgi is described
by the paper:
@InProceedings{StoughtonA:porgi,
author = "Allen Stoughton",
title = "porgi: a {P}roof-{O}r-{R}efutation {G}enerator for
{I}ntuitionistic propositional logic",
booktitle = "CADE-13 Workshop on Proof Search in Type-Theoretic
Languages",
year = 1996,
location = "Rutgers University",
month = "July",
pages = "109--116",
url="ftp://ftp.cis.ksu.edu/pub/CIS/Stoughton/porgi.ps.gz"
}
Resource requirements:
Implemented in Standard ML (SML/NJ Version 0.93), but produces a UNIX
command (see below), which can be invoked from the shell.
Where-to-get-it:
Porgi can be obtained---in both source and binary (SPARC/Solaris)
forms---via WWW URL http://www.cis.ksu.edu/~allen/porgi.html.
[Allen Stoughton, 6 August 1996]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%