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.

Sign up for GitHub

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

Jump to bottom

SZS status GaveUp and new line for -dkterm #40

Merged
merged 20 commits into from
Sep 17, 2024
Merged

SZS status GaveUp and new line for -dkterm #40

merged 20 commits into from
Sep 17, 2024

Commits on Jun 25, 2024

  1. Accept integers as formula names

    Guillaume Burel committed Jun 25, 2024
    Configuration menu
    Copy the full SHA
    bd90828 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'Deducteam:modulo' into modulo

    @gburel
    gburel authored Jun 25, 2024
    Configuration menu
    Copy the full SHA
    72754ae View commit details
    Browse the repository at this point in the history

Commits on Jul 11, 2024

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

    Guillaume Burel committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    01c06cd View commit details
    Browse the repository at this point in the history

  2. Merge branch 'modulo' of github.com:Deducteam/zenon_modulo into modulo

    Guillaume Burel committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    9ffe149 View commit details
    Browse the repository at this point in the history

Commits on Jul 14, 2024

  1. More close to real TPTP syntax of annotations. 

    (Still missing: formula_data, and semantic verification.)
    Guillaume Burel committed Jul 14, 2024
    Configuration menu
    Copy the full SHA
    5b82f2d View commit details
    Browse the repository at this point in the history

Commits on Sep 11, 2024

  1. add support for dune (Deducteam#24)

    @fblanqui
    fblanqui authored and Guillaume Burel committed Sep 11, 2024
    Configuration menu
    Copy the full SHA
    346cb80 View commit details
    Browse the repository at this point in the history

  2. change lp output to use the lambdapi-zenon library (Deducteam#33)

    @fblanqui
    fblanqui authored and Guillaume Burel committed Sep 11, 2024
    Configuration menu
    Copy the full SHA
    375d950 View commit details
    Browse the repository at this point in the history

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

    @fblanqui
    fblanqui authored and Guillaume Burel committed Sep 11, 2024
    Configuration menu
    Copy the full SHA
    b88bbae View commit details
    Browse the repository at this point in the history

  4. rename dummy_var into negated_conjecture (Deducteam#36)

    @fblanqui
    fblanqui authored and Guillaume Burel committed Sep 11, 2024
    Configuration menu
    Copy the full SHA
    84d23e9 View commit details
    Browse the repository at this point in the history

  5. fix dk output for GDV (Deducteam#37)

    @fblanqui
    fblanqui authored and Guillaume Burel committed Sep 11, 2024
    Configuration menu
    Copy the full SHA
    2e812e8 View commit details
    Browse the repository at this point in the history

  6. Merge branch 'Deducteam:modulo' into modulo

    @gburel
    gburel authored Sep 11, 2024
    Configuration menu
    Copy the full SHA
    20cfe2c View commit details
    Browse the repository at this point in the history

  7. Add SZS status in the output

    Guillaume Burel committed Sep 11, 2024
    Configuration menu
    Copy the full SHA
    69b5c37 View commit details
    Browse the repository at this point in the history

  8. Merge branch 'szs' into modulo

    Guillaume Burel committed Sep 11, 2024
    Configuration menu
    Copy the full SHA
    e9aeb1f View commit details
    Browse the repository at this point in the history

Commits on Sep 16, 2024

  1. Add -szs option 

    Add SZS dataform markers around proofs when -szs is set
Only print SZS status when -szs is set
    Guillaume Burel committed Sep 16, 2024
    Configuration menu
    Copy the full SHA
    4c246a4 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'szs' into modulo

    Guillaume Burel committed Sep 16, 2024
    Configuration menu
    Copy the full SHA
    38b1ae3 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'modulo' of github.com:Deducteam/zenon_modulo into modulo

    Guillaume Burel committed Sep 16, 2024
    Configuration menu
    Copy the full SHA
    2dd358d View commit details
    Browse the repository at this point in the history

Commits on Sep 17, 2024

  1. Output SZS status GaveUp when the proof search space is exhausted

    Guillaume Burel committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    e668717 View commit details
    Browse the repository at this point in the history

  2. Add new line at the end of -dkterm output

    Guillaume Burel committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    42bd41f View commit details
    Browse the repository at this point in the history

  3. Merge branch 'szs' into modulo

    Guillaume Burel committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    a0e9549 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'modulo' of github.com:Deducteam/zenon_modulo into modulo

    Guillaume Burel committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    044da0c View commit details
    Browse the repository at this point in the history