Filewatcher File Search File Search
Catalog
Content Search
» » » » »

spass

An automated theorem prover for first-order logic with equality

Variants:
SPASS is a saturation-based automated theorem prover for first-order logic with equality. It is unique due to the combination of the superposition calculus with specific inference/reduction rules for sorts (types) and a splitting rule for case analysis motivated by the beta-rule of analytic tableaux and the case analysis employed in the Davis-Putnam procedure. Furthermore, SPASS provides a sophisticated clause normal form translation.

This package consists of the SPASS/FLOTTER binary, documentation, and a small example collection. The tools collections contain the proof checker pcs, the syntax translators dfg2otter and dfg2tptp, and the ASCII pretty printer dfg2ascii.

For more information, additional and partly huge example collections, consider the project homepage at http://spass.mpi-sb.mpg.de/.

Homepage:-
Package version:3.7-2
Architecture:i386
Distribution:Debian
Filename:spass_3.7-2_i386.deb

/usr/share/doc/spass/README

				Welcome to SPASS!
				=================

This is the generic README file for all SPASS distributions, so your downloaded
package may only contain a subset of what is described here.


				Important Files
				===============

INSTALLATION 	for a guide to install the prover, man pages,
             	tools etc.; by default binaries are installed
		in /usr/local/bin and man-pages in /usr/local/man
more»

/usr/share/man/man1/SPASS.1.gz

SPASS(1)                        SPASS                       SPASS(1)



NAME
       SPASS - automated theorem prover for full first-order logic
       with equality

SYNOPSIS
       SPASS [options] [inputfile]

DESCRIPTION
       SPASS is an automated theorem prover for full sorted first-
       order logic with equality that extends superposition by sorts
       and a splitting rule for case anal
more»

/usr/share/man/man1/dfg2ascii.1.gz

DFG2ASCII(1)                    SPASS                   DFG2ASCII(1)



NAME
       dfg2ascii - transforms DFG files into pretty printed ASCII
       files

SYNOPSIS
       dfg2ascii <infile>

DESCRIPTION
       dfg2ascii is a program to convert a problem input file in DFG
       format into pretty-printed ASCII text. It prints out the
       axioms and the conjectures, in that order.

SEE ALSO
  
more»

/usr/share/man/man1/dfg2dfg.1.gz

DFG2DFG(1)                      SPASS                     DFG2DFG(1)



NAME
       dfg2dfg - calcul
more»

/usr/share/man/man1/dfg2otter.1.gz

DFG2OTTER(1)                    SPASS                   DFG2OTTER(1)



NAME
       dfg2otter - tran
more»

/usr/share/man/man1/dfg2otter.pl.1.gz

DFG2OTTER.PL(1)                 SPASS                DFG2OTTER.PL(1)



NAME
       dfg2otter - tran
more»

/usr/share/man/man1/dfg2tptp.1.gz

DFG2TPTP(1)                     SPASS                    DFG2TPTP(1)



NAME
       dfg2tptp - trans
more»

/usr/share/man/man1/tptp2dfg.1.gz

TPTP2DFG(1)                     SPASS                    TPTP2DFG(1)



NAME
       tptp2dfg - trans
more»

Browse inside spass_3.7-2_i386.deb

         [DIR]DEBIAN/ (2)  65535+ mirrors
         [DIR]usr/ (2)  65535+ mirrors

Download spass_3.7-2_i386.deb

Results 1 - 1 of 1
Help - FTP Sites List - Software Dir.
Search over 15 billion files
© 1997-2016 FileWatcher.com