=Overview= The Pangolin programming language is a functional language. In this language, the programmer can write logic assertions about the computed values. These assertions are proven statically, which ensures that the program is correct with respect to its specification. =Installation= =...

A resolution based theorem prover for first-order logic with equality. TPTP format is used for both problem input and proof output. Problems can be in clause (CNF) or general first-order (FOF) form. Inference rules used are binary resolution, factoring and paramodulation. Performance is as yet...

This suite of tools consists of: * hylores : a resolution-based theorem prover for the hybrid logic H(@,A,D,◇¯,↓) * htab : a tableaux-based theorem prover for the hybrid logic H(@,A,D,◇¯,↓) with role inclusion * hylolib : the common library used by the other provers * gridtest : a framewor...

=Eviva= It can revolutionarize how we develop applications. Initial thoughts are being shaped and a prototype is being built here on Google Code. Development began fall of 2009. Expect 2+ years to pass before anything useful appears, and 5 years before something really mature surfaces. ==...

Rapture automatically proves theorems using resolution engine. In current incarnation it implements a naive resolutions method for a subset of first-order logic, which allows it to prove simple facts. Rapture is implemented in C# 3.0 and currently supports only Microsoft .NET Framework of version...

The Inference Web is a Semantic Web based knowledge provenance infrastructure that supports interoperable explanations of sources, assumptions, learned information, and answers as an enabler for trust. * Provenance - if users (humans and agents) are to use and integrate data from unknown, unce...

reelkrlekrùmlk

CheQED is a proof assistant.

Here is a piece of software related to the paper: Extended Static Checking of Functional Programs We present a Hoare logic for a programming language equipped with recursive, higher-order functions, algebraic data types, and a polymorphic type system in the style of Hindley and Milner. It is t...

mymms aims at the implementation of * a high-ordered typed lambda calculus (CiC) * a proof editing mode * a set of certified decision procedure (mainly oracles for the type checking) Require ocaml >= 3.10 No documentation yet, but there is a begining tutorial, please look at ...