Subject: Logic software
From: "Eric J. Forbis" <[email-masked]>
To: Josef Eschgfaeller <[email-masked]>

I've received a steady stream of requests for information about theorem         
provers in response to my request on the APA BBS; below is a list of            
the programs I've seen thusfar. Pretty skimpy, I'm afraid. Several              
logic/AI conventions are being held this summer (notices have been posted       
on this list), which may make it easier to track down programs.                 
Commercial programs are unintentionally underrepresented. If you're aware       
of other programs, public or commercial, please drop a note or update           
the list.  

Logic programs and teaching aids, theorem provers and languages.                
                                                                                
1. MacLogic
   Uses symbolic logic notation. Working demo of classical logic for Macs,      
   modal logic disabled.                                                        
   ftp.st-and.ac.uk                                                             
2. *Nqthm                                                                       
   Boyer- Moore theorem prover (see book by same authors).                      
   Rascal.ics.utexas.edu :/pub/nqthm                                            
3. *Proof-checker                                                               
   rascal.ics.utexas.edu :/pub/proof-checker                                    
4. *Otter                                                                       
   Herky.cs.uiowa.edu :/public/otter                                            
5. *DTP                                                                         
   meta.stanford.edu :/pub/dtp                                                  
6. **Setheo
   flop.informatik.tu-muenchen.de :/pub/fki                                     
7. *HOL (Higher Order Language)                                                 
   ftp.cs.tut.fi :/pub/src/DisCo/hol90.6    Used to be available from           
   ftp.uidaho.edu :/pub/hol, but didn't see it there 2/94                       
8. LogicWorks  College level intro logic, commercial program.                   
   700 Excersizes and programs, $18 demo (?), DOS 2.0+                          
   Philosophical Documentation Center                                           
   Bowling Green State University                                               
   Bowling Green, OH 43403-0189                                                 
   (800) 444-2419                                                               
9. Logic: A Workbook  Teaches college level symbolic logic                      
   Commercial, price unknown, DOS 2.0+                                          
   Logic Software Project                                                       
   Department of Philosophy                                                     
   University of California, Los Angeles                                        
   Los Angeles, CA 90024-1451                                                   
   (213) 825-4641                                                               
                                                                                
* Requires LISP. Kyoto Common Lisp seems to be widely compatible
  with most of the above. It's conveniently available from                      
  rascal.ics.utexas.edu, amoung many other sites, and is available on all       
  platforms.                                                                    
** Requires Scheme. Available at this site (flop.informatik....).               
                                                                                
Items untrackable thusfar:                                                      
NuPRL  (by Martin & Lof)                                                        
PTTP
*         *          *                                                          
                                                                                
Regards,                                                                        
-=-=-=-=-=-=-=-=-=-=-=-=                                                        
Eric J. Forbis                                                                  
[email-masked]               
---

		The High Performance Theorem Prover
 
			*** S E T H E O ***
 
After several new developments concerning SETHEO and its components we 
are now able to provide the modified and updated version 
			   SETHEO V3.0 .
 
SETHEO V3.0  consists of a set of binaries for Sun Sparc computers, 
manpages, and a set of example problems.
 
SETHEO V3.0 can be obtained via FTP as follows:
 
	% ftp 131.159.8.35	(or "ftp flop.informatik.tu-muenchen.de")
 
	Name: anonymous
	Password: <your-e-mail-address>
 
	ftp> cd pub/fki
	ftp> binary
	ftp> get setheo.info
	ftp> get setheo.tar.Z
	ftp> bye

If you have any further questions please contact
 
         EMAIL: [email-masked]
 
         SNAIL: Intellektik
                Attn. M. Moser
                Technische Universitaet Muenchen
		Institut fuer Informatik
                Augustenstr. 46 RGB
                8000 Muenchen 2
                Germany

Good Luck,
	and much fun with
	
		SETHEO

About SETHEO:
============
 
SETHEO [Letz1992] is an automated theorem prover for formulae of predicate
logic. The first version of this SEquential THEOrem prover was developed in 
the ESPRIT-project 415 ''Parallel Architectures and Languages for Advanced 
Information Processing'' at the chair of computer architecture of the
Institut f"ur Informatik at the Technical University Munich.
 
SETHEO is based on the calculus of so called ``connection tableaux'', 
which can be seen as an efficient integration of the tableau calculus
[Smullyan1968], model elimination [Loveland1968] and the
connection method [Bibel1987] and is very well suited for automated theorem
proving.
 
The way SETHEO works differs basically from that of traditional resolution
based theorem provers and its today best known protagonist OTTER [McCune1988].
While resolution based theorem provers ensure the finding of a proof
by some kind of breadth-first-search, SETHEO performs depth-first-search 
controlled by backtracking. In order to ensure the completeness of the
proof procedure, in each `iteration' just finite parts of the search space 
are explored which are systematically increased in case of no success. 
This technique, commonly called `iterative deepening', was first implemented 
in the PTTP system of Stickel [Stickel1988].
 
The basic concept --`proof enumeration' instead of `formula enumeration'--
allows to use extremely refined variants of the calculus offering thus 
stronger search space reductions. 
 
Due to the success of prototypical versions of these refined variants,
which has been proven in many experiments, we have decided to
integrate them into the  
new system, SETHEO 3.0, which has been released in the spring of 93. 
SETHEO 3.0 provides `constraint techniques' which allow to impose structural 
restrictions on proofs in the model elimination calculus, the basic calculus 
of our system. 
 
The new techniques guarantee that in the proofs to be constructed
no clause is used in a tautological instance, nor in a instance
which can be subsumed. Furthermore the so called `regularity condition' 
ensures that all the literals in a path of a final tableau are
different, thus reducing considerably the search space.
By using `antilemma constraints' repeated solutions of subgoals resulting 
in the same answer substitution are avoided.
 
The constraints we use can be seen as disequations of termlists. 
Whenever a variable is instantiated during the proof process, the 
relevant constraints for the variable are inspected and updated. 
The constraint checks are incorporated very elegantly into the unification 
subroutine of our prover. For efficiency the constraint set is always kept 
in `solved form', i.e. all the constraints belonging to the variables 
can be accessed very quickly. Constraints which no longer be violated 
are dynamically removed from the constraint set. 
 
The above techniques ensure that far less proofs have to be enumerated, 
and lots of infinite branches of the search space are eliminated.  
 
Tautology and subsumption constraints for the clauses are automatically 
generated in a preprocessing phase. The so called regularity constraints, 
however, and the antilemma constraints have to be generated dynamically during 
the proof search. However, constraints can be also added to the clauses of 
the input formula. This together with the concept of `global variables'
(with destructive assignment) may be useful if you plan to use SETHEO as 
a tool for logic programming. In contrast to assert and retract in Prolog
SETHEO's global variables have a clear decarative semantics. 
 
The global variables can be used to describe `changing worlds'. They are 
are automatically backtracked during the proof search. The final proof which 
eventually expresses a plan can be visualized by a proof display program.  
 
To achieve high efficiencey the main proof procedure of SETHEO is based 
on a Prolog-like compilation technique. The input formulae are transformed 
into instructions of an abstract register-based machine. The underlying 
abstract machine is an extension and a modified variant of the 
`Warren Abstract Machine' [Warren1983] as it is used in many
professional Prolog systems today.
 
Due to its highly efficient technique of implementation, SETHEO attains
inference rates up to 70000 per second on standard sequential hardware
(SUN Sparc 1 Workstation). 
 
The system developed so far can be seen as an intermediate version. 
In the future we plan to integrate a more powerful constraint
generation module in preprocessing phase. In order to get shorter
proofs we plan to use lemmata - and last not least more intelligent 
search techniques have to be implemented to improve the
naive `iterative deepening' approach. 
 
Bibliography:
=============
 
[Bibel1987] W.~Bibel.  
Automated Theorem Proving.
Vieweg Verlag, Braunschweig, second edition, 1987.
 
[Letz1992] R.~Letz, J.~Schumann, S.~Bayerl, and W.~Bibel.
SETHEO: A High-Performance Theorem Prover.
Journal of Automated Reasoning, 8(2):183--212, 1992.
 
[Loveland1968] D.~W.~Loveland.
Mechanical Theorem Proving by Model Elimination.
Journal of the Association for Computing Machinery, 15(2):236--2 51, 1968.
 
[McCune1988] W.~McCune.
OTTER Users' Guide.
Technical report, Mathematics and Computer Sci. Division, Argonne
  National Laboratory, Argonne, Ill., USA, May 1988.
 
[Smullyan1968} R.~M.~Smullyan.
First Order Logic. Springer, 1968.
 
{Stickel1988] M.~A.~Stickel.
A Prolog Technology Theorem Prover: 
	Implementation by an Extended Prolog Compiler.
Journal of Automated Reasoning, 4:353--380, 1988.
 
[Warren1983} D.~H.~D. Warren.
An Abstract PROLOG Instruction Set.
Technical report, SRI, Menlo Park, California, USA, 1983.
---
Below is an abridged, intermediate version of the list of educational           
logic programs and theorem provers I recently posted. Several new entries       
have been added, and an address (MacLogic) corrected.
                                                                                
I hope to add at least 4 new entries in the near future, straighten up          
the format, obtain addresses, add a paragraph- long description for             
each entry, and add a 3rd section listing professional journals that            
advertise or review logic software. If you're aware of programs that 
should be included, addresses, or are able to comment on the programs,          
please send email.                                                              
                                                                                
-----Begin abridged list-------------------------------                         
                                                                                
Logic programs and teaching aids, theorem provers and languages.                
                                                                                
=-=-=-Public Domain Programs-- most are theorem provers.=-=-=-=-=-=-=-=         
                                                                                
1. PROOFCHK                                                                     
   For use with the Shaum's _Outline of Logic_, natural deduction.              
   Student enters proof and the theorem prover (a help button) offers           
   graded series of hints for solutions. Also includes a validity               
   checker and help screens.                                                    
       Send a disk and self- addressed stamped mailer to:                       
       John Nolt                                                                
       Philosophy Department                                                    
       University of Tennessee                                                  
       Knoxville, TN 37996-0480
                                                                                
2. *Nqthm                                                                       
   Boyer- Moore theorem prover (see book by same authors).                      
   Rascal.ics.utexas.edu :/pub/nqthm                                            
                                                                                
3. *Proof-checker                                                               
   rascal.ics.utexas.edu :/pub/proof-checker                                    
                                                                                
4. *Otter                                                                       
   Herky.cs.uiowa.edu :/public/otter                                            
                                                                                
5. *DTP                                                                         
   meta.stanford.edu :/pub/dtp
                                                                                
6. **Setheo                                                                     
   flop.informatik.tu-muenchen.de :/pub/fki                                     
                                                                                
7. *HOL (Higher Order Language)                                                 
   ftp.cs.tut.fi :/pub/src/DisCo/hol90.6    Used to be available from
   ftp.uidaho.edu :/pub/hol, but didn't see it there 2/94                       

8. MacLL
    "MacLogic-like proof editor for linear logic", by Roy Dyckhoff              
    and the MALT (Machine Assisted Logic Teaching) project at                   
    St. Andrew's University.                                                    
    138.251.192.40 (tamdhu.dcs.st-and.ac.au) :/pub/malt/macLL. Also             
    get MacLogic fonts from /pub/malt/maclogic.                                 

* Requires LISP. Kyoto Common Lisp seems to be widely compatible                
  with most of the above. It's conveniently available from                      
  rascal.ics.utexas.edu, amoung many other sites, and has been ported to        
  most operating systems.                                                       
** Requires Scheme. Available at this site (flop.informatik....).               

                                                                                
=-=-=-Commercial Programs-- Both educational and theorem provers.=-=-=-         
Most of these use symbolic logic notation, rather than lisp or prolog.          
                                                                                
1. MacLogic
   Minimal, intuitionistic, classical propositional & predicate                 
   calculi, with theorem provers.                                               
   Macintosh                                                                    
   Contact Roy Dyckhoff, the author, at [email-masked] for                 
   an informational sheet with directions for ftping.                           

2. LogicWorks  College level intro logic.                                       
   700 Excersizes and programs, $18 demo (?), DOS 2.0+                          
   Philosophical Documentation Center                                           
   Bowling Green State University                                               
   Bowling Green, OH 43403-0189                                                 
   (800) 444-2419                                                               
                                                                                
3. Logic: A Workbook
   Teaches college level symbolic logic.                                        
   Price unknown, DOS 2.0+.                                                     
   Logic Software Project                                                       
   Department of Philosophy
   University of California, Los Angeles                                        
   Los Angeles, CA 90024-1451                                                   
   (213) 825-4641                                                               
                                                                                
4. LogicCoach                                                                   
   Educational software for the Hurley and Kahane logic texts. User             
   friendly proof checker through 1st order functional calculus w/identity.     
   Distributed by the Wadsworth Publishing Company.                             
                                                                                
5. Symlog
   College level symbolic logic educational software designed to be             
   used with _Logic with Symlog_, Frederic Portoraro and Robert Tulley.         
   Distributed by Prentice- Hall.                
6. Tarski's World 4.0                                                           
   1st order logic educational software to supplement any standard              
   logic text. Represents logical propositions in graphical worlds,             
   manual and exercises. By Jon Barwise and John Etchemendy.                    
   Macintosh and Windows, $19.50                                                
   Distributed by the University of Chicago Press. For more information,        
   contact Dean Blobaum at [email-masked].                         
                                                                                
7. The Language of First- Order Logic_, 3rd edition.                            
   A 1st order symbolic logic text that includes Tarski's World 4.0.            
   Macintosh and Windows, $34.95                                                
   Distributed by the University of Chicago Press. For more information,        
   contact Dean Blobaum at [email-masked].                         
                                                                                
8. Turing's World 3.0: Introduction to Computability Theory                     
   Software for diagramming Turing machines, includes short text                
   on Turing machines with software- integrated exercises.                      
   Macintosh, $19.95                                                            
   Distributed by the University of Chicago Press. For more information,
   contact Dean Blobaum at [email-masked].                         
                                                                                
9. Hyperproof                                                                   
   Text and software for analytic reasoning, can be used with items             
   6 and 7 in this section. "Combines graphical and sentential                  
   information, and presents a set of logical rules for integrating             
   these different forms of information."                                       
   Macintosh, $24.95                                                            
   Distributed by the University of Chicago Press. For more information,        
   contact Dean Blobaum at [email-masked].                         

Unknown programs:                                                               
NuPRL  (by Martin & Lof)                                                        
PTTP
                                                                                
=-=-=-=-=Journals=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-                                 
                                                                                
1. Philosophy and Computer Newsletter
   Carnegie Mellon University
                                                                                
------------End abridged list-------------------------------                    
-=-=-=-=-=-=-=-=-=-=-=-=                                                        
Eric J. Forbis                                                                  
[email-masked] 
---