|
Home >> Science >> Math >> Logic and Foundations >> Software |
|
LWB Logics Workbench. SwitchMin Digital Circuit Minimizer Tool for minimizing boolean logic functions. 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. Bertrand First-order satisfiability checker and prover for the Macintosh. 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. Automated Reasoning Project Web resource provided by research group. Includes access to software developed by the team, coverering such projects as FINDER (Finite Domain Enumerator), MaGIC (Matrix Generator for Implication Connectives) and Kripke (A theorem prover for the relevant logic LR). MUltseq A generic sequent prover for propositional finitely-valued logics. MUltlog Takes as input the specification of a finitely-valued first-order logic and produces a sequent calculus, a natural deduction system, and clause formation rules for this logic. Isabelle A generic theorem proving environment developed at Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow). Includes logic, documentation and free download. WinKE: A Proof Assistant for Teaching Logic WinKE is 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. |
|
© 2005 GeneralAnswers.org