- 04 Jul, 2018 3 commits
-
-
Raphael Cauderlier authored
-
Raphael Cauderlier authored
-
Raphael CAUDERLIER authored
compatibility with Dedukti 2.6 See merge request cauderlier/dktactics!1
-
- 03 Jul, 2018 1 commit
-
-
François Thiré authored
-
- 14 May, 2018 3 commits
-
-
Raphael Cauderlier authored
-
Raphael Cauderlier authored
-
Raphael Cauderlier authored
-
- 10 May, 2018 3 commits
-
-
Raphael Cauderlier authored
-
Raphael Cauderlier authored
-
Raphael Cauderlier authored
This is probably a bit more portable
-
- 05 May, 2018 2 commits
-
-
Raphael Cauderlier authored
-
Raphael Cauderlier authored
-
- 02 Feb, 2018 9 commits
-
-
Raphael Cauderlier authored
-
Raphael Cauderlier authored
-
Raphael Cauderlier authored
-
Raphael Cauderlier authored
-
Raphael Cauderlier authored
-
Raphael Cauderlier authored
-
Raphael Cauderlier authored
update installation instructions
-
Raphael Cauderlier authored
-
Raphael Cauderlier authored
-
- 01 Feb, 2018 2 commits
-
-
Raphael Cauderlier authored
This is the smallest proof produced by prover9 that uses both rules of resolution.
-
Raphael Cauderlier authored
did not reduce
-
- 31 Jan, 2018 1 commit
-
-
Raphael Cauderlier authored
-
- 30 Jan, 2018 1 commit
-
-
Raphael Cauderlier authored
-
- 28 Jan, 2018 1 commit
-
-
Raphael Cauderlier authored
-
- 27 Jan, 2018 1 commit
-
-
Raphael Cauderlier authored
-
- 26 Jan, 2018 5 commits
-
-
Raphael Cauderlier authored
-
Raphael CAUDERLIER authored
-
Raphael CAUDERLIER authored
-
Raphael CAUDERLIER authored
-
Raphael CAUDERLIER authored
-
- 25 Jan, 2018 3 commits
-
-
Raphael Cauderlier authored
-
Raphael Cauderlier authored
-
Raphael Cauderlier authored
-
- 23 Jan, 2018 3 commits
-
-
Raphael Cauderlier authored
A dependent substitution is a substitution from formulae to formulae that can act depend on the topmost universally quantified variables of the formula. This is going to be useful for handling substitutions of clauses.
-
Raphael Cauderlier authored
-
Raphael Cauderlier authored
-
- 14 Dec, 2017 2 commits
-
-
Raphael Cauderlier authored
-
Raphael Cauderlier authored
This structure is intended to be used for resolution and paramodulation tactics. Having both clauses under the same quantifiers allows to perform shallow unification.
-