@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@

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] 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%