satore

First order logic theorem prover in CNF without equality but with atom rewrite rules

Build status: ok passing tests

Authors

laurent.orseau@gmail.com

Documentation

satore

Tags

logic

Last updated

Thursday, July 15th, 2021 6:35:43pm (UTC)

Ring

1

Conflicts

None

Dependencies

Most recent build results

Compiled successfully: transcript
Tests succeeded: transcript

Version Exceptions

Version	Source	Checksum
default	https://github.com/deepmind/deepmind-research.git?path=satore	18fe509b50b862f922f0e04e9dd1d0c7d4ba62a8

Last checked

Saturday, July 24th, 2021 10:42:16pm (UTC)

Last edited

Tuesday, March 9th, 2021 4:31:22pm (UTC)

Date added

Tuesday, March 9th, 2021 4:17:43pm (UTC)

Modules

satore/main.rkt
satore/log.rkt
satore/tests/unification.rkt
satore/Clause.rkt
satore/scribblings/satore.scrbl
satore/rewrite-tree.rkt
satore/clause.rkt
satore/tests/trie.rkt
satore/tests/rewrite-tree.rkt
satore/saturation.rkt
satore/tests/Clause.rkt
satore/tests/saturation.rkt
satore/tptp.rkt
satore/unification-tree.rkt
satore/tests/stress-test1.rkt
satore/tests/confluence.rkt
satore/trie.rkt
satore/interact.rkt
satore/tests/unification-tree.rkt
satore/json-output.rkt
satore/misc.rkt
satore/unification.rkt
satore/clause-format.rkt
satore/tests/misc.rkt
satore/tests/interact.rkt
satore/tests/clause.rkt