https://e-sygoing.link Latest links in the Software category en-us Sun, 24 May 2026 00:50:14 -0400 https://e-sygoing.link/link/5285017-database-of-existing-mechanized-reasoning-systems A list (>50 entries) of automatic resolution provers (like Otter), interactive provers (like PVS) and other mechanized reasoning tools. Wed, 05 Nov 2025 15:50:00 -0500 https://e-sygoing.link/go/5285017 https://e-sygoing.link/link/5285038-church Program understands the different types of lambda expressions, can extract lists of variables (both free and bound) and subterms, and can simplify complicated expressions. Uses Python. Sun, 03 Aug 2025 05:14:40 -0400 https://e-sygoing.link/go/5285038 https://e-sygoing.link/link/5285034-dc-proof-online New proof-writing software to teach the fundamentals of logic and proof. Enables users/students to write error-free proofs by selecting rules of inference, axioms, etc. from convenient drop-down menus. Includes tutorial and exercises. Mon, 16 Jun 2025 07:48:33 -0400 https://e-sygoing.link/go/5285034 https://e-sygoing.link/link/5285029-acl2-version-27 A programming language in which you can model computer systems and a tool to help prove properties of those models. Available under GPL and runs on various platforms. Includes related download links. Tue, 20 May 2025 01:05:00 -0400 https://e-sygoing.link/go/5285029 https://e-sygoing.link/link/5285015-protein A PROver with a Theory Extension INterface. Theorem prover for first-order clause logic, written in ECRC's Prolog-dialect ECLiPSe. Free download, documentation. Wed, 09 Apr 2025 17:03:59 -0400 https://e-sygoing.link/go/5285015 https://e-sygoing.link/link/5285024-proofpower A suite of tools supporting specification and proof in Higher Order Logic (HOL) and in Z notation. Tue, 08 Apr 2025 04:19:28 -0400 https://e-sygoing.link/go/5285024 https://e-sygoing.link/link/5285025-loom A language and environment for constructing intelligent applications. It is a research project in the Artificial Intelligence research group at the University of Southern California's Information Sciences Institute. The goal of the project is to develop and field advanced tools for knowledge representation and reasoning in Artificial Intelligence. Sat, 29 Mar 2025 05:10:41 -0400 https://e-sygoing.link/go/5285025 https://e-sygoing.link/link/5285019-multseq A generic sequent prover for propositional finitely-valued logics. Sat, 31 Aug 2024 10:46:03 -0400 https://e-sygoing.link/go/5285019 https://e-sygoing.link/link/5285037-proof-general Comprehensive Gnu-Emacs and XEmacs interface for several theorem provers including Coq, Isabelle, Lego, and Phox. Sat, 01 Jun 2024 00:50:39 -0400 https://e-sygoing.link/go/5285037 https://e-sygoing.link/link/5285039-winke An interactive proof assistant based on analytic tableaux, and designed for the teaching of deductive reasoning. Ordering information is available at this site, as are academic papers on the design of the software. Fri, 31 May 2024 22:03:20 -0400 https://e-sygoing.link/go/5285039