prover9

Description

Automated theorem prover for first-order and equational logic.

Prover9 is a resolution/paramodulation automated theorem prover for first-order and equational logic. Prover9 is a successor of the Otter Prover. This is the LADR command-line version.

Metadata

Version

2009-11a

Executables (39)

Show all

bin/attack
bin/autosketches4
bin/clausefilter

bin/clausetester
bin/complex
bin/directproof
bin/dprofiles
bin/fof-prover9
bin/gen_trc_defs
bin/get_givens
bin/get_interps
bin/get_kept
bin/idfilter
bin/interpfilter
bin/interpformat
bin/isofilter
bin/isofilter0
bin/isofilter2
bin/ladr_to_tptp
bin/latfilter
bin/looper
bin/mace4
bin/miniscope
bin/mirror-flip
bin/newauto
bin/newsax
bin/olfilter
bin/perm3
bin/prooftrans
bin/prover9
bin/prover9-mace4
bin/renamer
bin/rewriter
bin/sigtest
bin/test_clause_eval
bin/test_complex
bin/tptp_to_ladr
bin/unfast
bin/upper-covers

Platforms (21)

Linux

Show all

aarch64-linux
armv5tel-linux
armv6l-linux
armv7a-linux
armv7l-linux
i686-linux
loongarch64-linux
m68k-linux
microblaze-linux
microblazeel-linux
mips-linux
mips64-linux
mips64el-linux
mipsel-linux
powerpc64-linux
powerpc64le-linux
riscv32-linux
riscv64-linux
s390-linux
s390x-linux
x86_64-linux

Version

License

Status

Source

Homepage

Executables39 (39)

Platforms21 (21)

Executables (39)

Platforms (21)