Correct behaviour for -gdv - #52

Merged

gburel merged 28 commits into

Deducteam:modulofrom

Jun 26, 2026

Commits on Jun 25, 2024

Accept integers as formula names
Guillaume Burel
committed
bd90828
Merge branch 'Deducteam:modulo' into modulo
gburel
authored
72754ae

Commits on Jul 11, 2024

Fix bug where a free variable was printed in the proof term.
Guillaume Burel
committed
01c06cd
Merge branch 'modulo' of github.com:Deducteam/zenon_modulo into modulo
Guillaume Burel
committed
9ffe149

Commits on Jul 14, 2024

More close to real TPTP syntax of annotations.
Guillaume Burel
committed
5b82f2d

Commits on Sep 11, 2024

add support for dune (#24)

fblanqui
authored and
Guillaume Burel
committed
346cb80
change lp output to use the lambdapi-zenon library (#33)

fblanqui
authored and
Guillaume Burel
committed
375d950
lltolp.ml: fix requires for lambdapi-zenon library (#35)

fblanqui
authored and
Guillaume Burel
committed
b88bbae
rename dummy_var into negated_conjecture (#36)

fblanqui
authored and
Guillaume Burel
committed
84d23e9
fix dk output for GDV (#37)

fblanqui
authored and
Guillaume Burel
committed
2e812e8
Merge branch 'Deducteam:modulo' into modulo
gburel
authored
20cfe2c
Add SZS status in the output
Guillaume Burel
committed
69b5c37
Merge branch 'szs' into modulo
Guillaume Burel
committed
e9aeb1f

Commits on Sep 16, 2024

Add -szs option
Guillaume Burel
committed
4c246a4
Merge branch 'szs' into modulo
Guillaume Burel
committed
38b1ae3
Merge branch 'modulo' of github.com:Deducteam/zenon_modulo into modulo
Guillaume Burel
committed
2dd358d

Commits on Sep 17, 2024

Output SZS status GaveUp when the proof search space is exhausted
Guillaume Burel
committed
e668717
Add new line at the end of -dkterm output
Guillaume Burel
committed
42bd41f
Merge branch 'szs' into modulo
Guillaume Burel
committed
a0e9549
Merge branch 'modulo' of github.com:Deducteam/zenon_modulo into modulo
Guillaume Burel
committed
044da0c

Commits on Jun 26, 2026

Parsing (and typing) of espilon-terms in TPTP input files
gburel
committed
2a04a24
Producing an annotation term for TPTP input
gburel
committed
c106883
WIP finding the name of a Skolem symbol from annotations
gburel
committed
85b2715
Merge branch 'modulo' of github.com:Deducteam/zenon_modulo into modulo
gburel
committed
95d24d2
Add annotation.ml to Makefile
gburel
committed
32f0aaf
New flag -gdv instead of flag -lp-package
gburel
committed
baea2d2
Correct behaviour for the -gdv flag
gburel
committed
6d576dd
Merge branch 'modulo' of github.com:Deducteam/zenon_modulo into modulo
gburel
committed
5d25804