Does Z3 support EPR logic with stratified function symbols? #6917
Unanswered
nicola-gigante
asked this question in
Q&A
Replies: 0 comments
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
There is an extension of the EPR fragment of first-order logic with functions symbols, as long as the sorts of the functions are structured in the right way. This is studied in this paper here (cited as [ARS10] below), and also cited in the PhD thesis by Voigt here. In the latter this is stated as follows:
Proposition 3.14.4 ([ARS10, GdM09, Kor13b]). The satisfiability problem for multi-sorted ∃*∀* sentences over a stratified vocabulary is decidable.
where a "stratified vocabulary" can contain function symbols but, indeed, with sorts structured accordingly.
If I'm not wrong, Z3 has ad-hoc procedures for the EPR fragment. Does it, by chance, support this extended fragment as well?
Beta Was this translation helpful? Give feedback.
All reactions