@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ 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] %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%