8000 Alethe proof uses `:named` in partially applied terms · Issue #11750 · cvc5/cvc5 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Alethe proof uses :named in partially applied terms #11750

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
Open
bpandreotti opened this issue Mar 19, 2025 · 0 comments
Open

Alethe proof uses :named in partially applied terms #11750

bpandreotti opened this issue Mar 19, 2025 · 0 comments
Assignees
@HanielB
Labels
experimental

Comments

@bpandreotti
Copy link

When printing an Alethe proof, cvc5 will sometimes name partially applied terms using the (! ... :named ...) construct, which (as I understand) is not allowed in Alethe. An example of this is the following problem:

(set-logic UF)
(declare-sort I 0)
(declare-fun m (I I) Bool)
(declare-fun s (I) I)
(assert (forall ((smt__b I) (smt__f I)) (! (or (m smt__f (s smt__b)) (not (= smt__b (s smt__f)))) :pattern ((s smt__f)))))
(assert (forall ((smt__f I)) (= smt__f (s smt__f))))
(declare-fun sm () I)
(assert (not (m sm (s sm))))
(check-sat)
(get-proof)

Running cvc5 on this problem with the options --produce-proofs --proof-format-mode=alethe --proof-granularity=dsl-rewrite, we get an Alethe proof that contains the term ((! (m smt__f) :named @p_21) @p_28), which uses :named on the partially applied term (m smt__f).

This was tested on commit ab64642.
@HanielB HanielB self-assigned this Mar 20, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@HanielB HanielB

Labels
experimental
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@HanielB @ajreynol @bpandreotti
0