theoremprover-museum/HOL88 theoremprover-museum/HOL88

  • Stars
    star
    9
  • Rank 1,939,727 (Top 39 %)
  • Language Standard ML
  • Created about 8 years ago
  • Updated about 8 years ago
Twitter logo Share LinkedIn logo Share Facebook logo Share
theoremprover-museum/HOL88
github

theoremprover-museum

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

The HOL System is an environment for interactive theorem proving in a higher-order logic. Its most outstanding feature is its high degree of programmability through the meta-language ML.

More Repositories

1

logic-theorist

The sources of the first theorem prover.
55
star
2

theoremprover-museum.github.io

HTML
51
star
3

LCF77

The original Edinburgh LCF.
Common Lisp
23
star
4

prover9

Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples.
C
15
star
5

OMEGA

A theorem prover for higher-order logic based on proof planning.
Isabelle
7
star
6

imps

The IMPS Theorem Prover
Perl 6
7
star
7

clam3

Prolog implementation of proof planner with critics, and some higher-order unification, in the v3 branch of Clam.
Prolog
6
star
8

EQP

EQP is an automated theorem proving program for first-order equational logic. Its strengths are good implementations of associative-commutative unification and matching, a variety of strategies for equational reasoning, and fast search.
C
5
star
9

InKa

InKa - an inductive theorem prover
Common Lisp
4
star
10

otter

The first theorem prover and model generator for first-order logic with equality from the Argonne group that was widely distributed.
C
4
star
11

HOL90

The source of hte HOL90 Theorem prover.
Standard ML
3
star
12

MKRP

The Markgraph Karl Refutation Procedure, a graph-based resolution theorem prover written in Common Lisp
Common Lisp
3
star
13

SETHEO

The SETHEO theorem prover (C version)
C
3
star
14

TPS

TPS is an interactive, semi-automatic, and automatic Theorem Proving System for first-order logic and higher-order logic. The subsystem ETPS is designed for interactive use by students in logic courses.
Common Lisp
3
star
15

LEGO

the source archive for LEGO: an interactive proof development system for various type theories
Lex
2
star
16

scunac

a proof checker and interactive theorem prover for dependently typed set theory
Common Lisp
2
star
17

lambdaclam

AMPL
2
star
18

egal

Chad Brown’s Egal, a theorem prover for higher-order Tarski–Grothendieck set theory
OCaml
2
star
19

muscadet

The Muscadet Theorem Prover is a knowledge-based system. Based on natural deduction, it uses methods which resemble those used by humans, implemented in one or several bases of facts. The output is an easily readable proof.
Prolog
2
star
20

SNARK

SNARK - SRI's New Automated Reasoning Kit
Common Lisp
1
star
21

ProCom

A theorem prover based on the PTTP paradigm.
Prolog
1
star
22

doc

Documentation about the Theorem Prover Museum
TeX
1
star
23

oleg

Standard ML
1
star
24

clam2

A Prolog implementation of the proof planner Clam (in the clam2 development branch) and the associated theorem prover, oyster.
Prolog
1
star