ELF Frank Pfenning et. al. Elf, a logic programming language based on the LF Logical Framework. Natural Semantics and Some of its Meta-Theory in ELF. Spiro Michaylov and Frank Pfenning. Technical Report MPI-I-91-211. Max-Planck-Institute for Computer-Science. Logic Programming in the LF Logical Framework. Frank Pfenning. First Workshop on Logical Frameworks. 1991 A Framework for Defining Logics. Robert Harper, Furio Honsel and Gordon Plotkin. Modularity in the LF Logical Framework. Robert Harper and Frank Pfenning. Second Workshop on Logical Frameworks. 1991 Implementing the Meta-Theory of Deductive Systems. Frank Pfenning and Ekkehard Rohwedder. LNAI 607. CADE-11. Springer-Verlag. 1993. Higher-Order Logic Programming as Constraint Logic Programming. Spiro Michaylov. alonzo.tip.cs.cmu.edu (/afs/cs/user/fp/public) Corre sobre o Standard ML. Instalado numa SUN 10 sem problems. HOL (Hol88 / Hol90) DSTO Australia, Cambridge University and SRI International The HOL systems supports Higher Order Logic. The HOL System: TUTORIAL, DSTO Australia and Cambridge University and SRI International, July 1991 The HOL System: DESCRIPTION, DSTO Australia and Cambridge University and SRI International, July 1991 The HOL System: REFERENCE, DSTO Australia and Cambridge University and SRI International, July 1991 The HOL System: LIBRARIES, DSTO Australia and Cambridge University and SRI International, July 1991 (ftp) ftp.informatik.tu-munchen.de HOL90 baseado no SML/NJ. Instalado numa SUN 10 sem problemas. ICLE (Imperial College Logic Environment) Mark Dawson The I.C.L.E. environment provides a direct way of defining and using a wide variety of logical systems. A logic is presented to the environment as a collection of rules over a specified language. Proofs can be conducted in the logic using strategies defined with respect to the rules available. Using the Imperial College Generic Logic Environment - a tutorial guide, Mark Dawson, Department of Computing, Imperial College, 11 October 1991. The Imperial College Logic Environment - Reference Manual, Mark Dawson. Deriving Rules with the Imperial Logic Environment, Mark Dawson, Department of Computing, Imperial College, May 1991, Technical Report DOC-91-39. Defining Logics with the Imperial College Logic Environment, Mark Dawson, Department of Computing, Imperial College, May 1991, Technical Report DOC-91-38. (ftp) theory.doc..ic.ac.uk:/theory/software/icle Instalado na Sun SparcStation 1 depois de resolvida a questao dos tipos de letras. O programa \'e ainda muito inst\'avel, por diversas vezes abortou a execu\c{c}\~ao. A instala\c{c}\~ao nao foi totalmente bem sucedida pois que nas l\'ogicas pr\'e-definidas o programa queixa-se de n\~ao encontrar os ficheiros (???). O apoio por parte do autor foi muito correcto e prof\'{\i}quo. Isabelle Lawrence C. Paulson (lcp@cl.cam.ac.uk) generic theorem prover supporting formal proofs in a variaty of logics" Introduction to Isabelle, Lawrence C. Paulson, Computer Laboratory University of Cambridge, 1992. Isabelle's Object-Logics, Lawrence C. Paulson, Computer Laboratory University of Cambridge, 1993. The Isabelle Reference Manual, Lawrence C. Paulson et. al., Computer Laboratory University of Cambridge, 1993. A Fixed Approach to Implementing (Co)Inductive Definitions, Lawrence C. Paulson , Computer Laboratory University of Cambridge, 25 November 1993. (ftp) gannet.cl.cam.ac.uk Implementado em ML (SML/NJ ou Poly/ML). Instala\c{c}\~ao sem problemas de qualquer um dos seus m\'odulos. O sistema j\'a tem implementados os seguintes sistemas l\'ogicos: FOL -- First Order Logic (intuicionista e cl\'assica); ZF -- Zermelo-Fraenkel Set Theory; CTT -- Constructive Type Theory; HOL -- Higher Order Logic; LK -- C\'alculo de Sequentes Cl\'assico; Modal -- L\'ogica Modal T, S3, S43; LCF -- Logic for Computable Functions (Teoria dos Dom\'{\i}nios; Cube -- Barendregt's Lambda Cube. 2OBJ Andrew Stevens and Keith Hobley "meta-logical framework theorem prover that can be programed to prove theorems in any desired logical system". Andrew Stevens and Keith Hobley, Mechanised Theorem Proving with 2OBJ: A Tutorial Introduction, Oxford University, 1993. Introducing OBJ3, Joseph A. Goguen and Timothy Winkler, Technical Report SRI-CSL-88-9, SRI International, Computer Science Lab, August 1988. OBJ as a Theorem Prover with Applications to Hardware Verification, Joseph Goguen, Technical Report SRI-CSL-88-4R2, SRI International, Computer Science Lab, August 1988. (ftp) ftp.comlab.ox.ac.uk:pub/Packages/2OBJ Necessita do OBJ3. Interface em X11. Instalado sem problemas com excep\c{c}\~ao do criar de uma imagem OBJ3 j\'a com o sistema 2OBJ pr\'e-carregado. O apoio por parte do autor \'e nulo. Por diversas vezes tentei entrar em contacto com o Andrews Stevens e ele nunca respondeu. O c\'alculo de sequentes tal como est\'a formalizado est\'a errado. O programa n\~ao possue nenhuma forma de automatiza\c{c}\~ao da prova. SETHEO J. Schumann Setheo is a theorem prover for full first order logic J. Schumann, man files for Setheo, sam, ... SETHEO V3.2: Recent Developments --- System Abstract. Chr. Goller, R. Letz, K. Mayr, J. Schumann. CADE-12. SETHEO: A High-Performance Theorem Prover. R. Letz, J. Schumann, S. Bayerl, and W. Bibel. Journal of Automated Reasoning, 8(2):183-212, 1992. (ftp) flop.informatik.tu-munchen.de Execut\'aveis para Sun Sparc (sun4). xsetheo requer o X-Windows. O apoio por parte do autor \'e bom. Estou numa "mailing list" referente ao programa. KEIM Daniel Nesmith KEIM is a collection of software modules, written in Common Lisp with CLOS, designed to be used in the production of theorem proving systems. KEIM is intended to be used by those who whant to build or use deduction systems (such as resolution theorem provers) without having to write the entire framework. KEIM is also suitable for embedding a reasoning component into another Common Lisp program. Using KEIM, Daniel Nesmith, August 28, 1993. Test-Keim Manual, The KEIM-Group, Fachbereich Informatik, Univesitat des Saarlandes, Germany, October 4, 1993. (europa) js-sfbsun.cs.uni-sb.de:pub/keim (N.America), ftp.cs.cmu.edu:/afs/cs/project/tps/keim N\~ao consegui fazer a instala\c{c}\~ao no CMU-Common Lisp 17 O apoio foi bom (o Common Lisp \'e que n\~ao). Faust Klaus Schneider, Ramayya Kumar, Thomas Kropf. ... "a set of provers called FAUST, for automatically proving first-order statements within HOL and a set of examples. All the FAUST-provers are based on a modified form of sequent calculus called ``Restricted Sequent Calculus'' and use first-order unification for computing terms for substitution during a gamma-rule application." Efficient Representation and Computation of Tableaux Proofs, Klaus Schneider, Ramayya Kumar and Thomas Kropf, Institute of Computer Design and Fault Tolerance, University of Karlsruhe, Germany. Structuring Hardware Proofs:First steps towards Automation is a Higher-Order Environment, Klaus Schneider, Ramayya Kumar and Thomas Kropf, Proc. VLSI'91, Edinburgh, Aug. 20-22. Hardware-Verification using First Order BDDs, Klaus Schneider, Ramayya Kumar and Thomas Kropf,University of Karlsruhe, Institute of Computer Design and Fault Tolerance, Germany. Automating most Parts of Hardware Proofs in HOL, Klaus Schneider, Ramayya Kumar and Thomas Krop, Proc. CAV'91, Aalborg Denmark, July 1-4, 1991. (ftp) goethe.ira.uka.de:/pub/papers/92_HUG_FAUST.ps.Z Requer o sistema HOL. J\'a consegui instalar o sistema numa Sparc tendo criado um executavel (gabriel). MERIL (M-ERIL-L) Brian Mattews MERILL is a general purpose order-sorted equational reasoning system M-ERIL-L: an equational Reasoning System in Standard ML. A User Guide (Draft). (ftp) ftp.dcs.gla.ac.uk (/pub/merill) rummerill (centelha) executavel, merill (gabriel) interpretador N\~ao \'e um provador de teoremas gen\'erico mas t\~ao somente um sistema de l\'ogica equational (como ele pr\'oprio diz). Ou seja julgo que n\~ao \'e poss\'{\i}vel construir um sistema l\'ogico de raiz e de seguida provar teoremas sobre ele.