Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

rename dummy_var into negated_conjecture #36

Merged
merged 1 commit into from
Jul 18, 2024

Conversation

fblanqui
Copy link
Member

No description provided.

@fblanqui fblanqui merged commit bf4213e into Deducteam:modulo Jul 18, 2024
10 checks passed
@fblanqui fblanqui deleted the dummy_var branch July 18, 2024 13:47
gburel pushed a commit to gburel/zenon_modulo that referenced this pull request Sep 11, 2024
gburel added a commit that referenced this pull request Sep 11, 2024
* Accept integers as formula names

* Fix bug where a free variable was printed in the proof term.

* More close to real TPTP syntax of annotations.
(Still missing: formula_data, and semantic verification.)

* add support for dune (#24)

* change lp output to use the lambdapi-zenon library (#33)

* lltolp.ml: fix requires for lambdapi-zenon library (#35)

* rename dummy_var into negated_conjecture (#36)

* fix dk output for GDV (#37)

* Add SZS status in the output

---------

Co-authored-by: Guillaume Burel <[email protected]>
Co-authored-by: Frédéric Blanqui <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant