240 questions
- Bountied 0
- Unanswered
- Frequent
- Score
- Trending
- Week
- Month
- Unanswered (my tags)
2
votes
1
answer
99
views
Quantifier introduction in Dafny: prove abs is surjective
This is a similar question but I haven't been able to map it to my use case.
Basically I want to use Dafny to prove a basic statement with nested quantifiers (for all X there exists Y) in first-order ...
0
votes
0
answers
35
views
T-SQL LIKE - quantifiers [duplicate]
I get passed manual user input and have to build format tests in SQL Server to check whether user input conforms to expected input.
For example, an ID should start with two capital letters followed by ...
0
votes
2
answers
479
views
Is there a parser from Python-Z3 to Z3/smt2?
I am working with the Python API of Z3, because of convenience, but sometimes I need to convert my Python results into readable input for Z3/smt2. For instance, whenever I perform quantifier ...
0
votes
0
answers
109
views
Exporting code for definitions with the universal quantifier in Isabelle
I’m trying to export code from the Isabelle theorem prover using its code extraction tools. The code I’m trying to extract is based on an integrity constraint that returns a boolean value from a ...
0
votes
1
answer
167
views
Express each of these statements in terms of C(x), D(x), F(x), quantifiers, and logical connectives
Let C(x) be the statement "x has a cat,"
let D(x) be the statement "x has a dog,"
let F(x) be the statement "x has a ferret."
Express each of these statements in terms of C(x), D(x), F(x), quantifiers,...
0
votes
1
answer
52
views
Searching Skolem functions in non-linear arithmetics
I found that the following paper/code (https://github.com/grigoryfedyukovich/aeval) solves Skolem function search for linear arithmetic. It performs really well.
However, I would like to compute ...
0
votes
1
answer
50
views
Does quantifier elimination preserve equi-satisfiability or equivalence? And in Z3?
Does quantifier elimination (QE) preserve equi-satisfiability or equivalence?
I always thought QE preserves equi-satisfiability (and not equivalence) but in the book [Bradley, Manna], they say both ...
0
votes
1
answer
126
views
If a theory is decidable in the existential fragment, does this mean that there is a (terminating) method to obtain witnesses of satisfaction?
I am concerned with whether there are algorithms (e.g., implemented in SMT solvers) that guarantee termination on the task of giving models of existential formulae; in the same way they guarantee ...
0
votes
1
answer
101
views
I think Z3 is not performing quantifier elimination in a sequence instance
Consider the following Z3 definition of an array average function:
IntSeqSort = SeqSort(IntSort())
sumArray = RecFunction('sumArray', IntSeqSort, IntSort())
sumArrayArg = FreshConst(IntSeqSort)
...
0
votes
1
answer
155
views
How can I perform validity of ∃∀.φ, if I use quantifier elimination for ∀.φ and get φ'? I hypothetise ∃φ' solves satisfiability, not validity
I want to check validity of a formula with the following quantifier alternation: ∃∀.φ
Do I check validity of this formula if I solve Exists(exist_vars, ForAll(forall_vars, Phi)) in Z3Py? What is the ...
2
votes
1
answer
92
views
How to define a data type with an explicit kind quantification?
When I define
data Foo a = Foo [a]
then the type is of kind Foo :: * -> *.
Having enabled PolyKinds and RankNTypes I'd like to explicitly quantify it with a more general kind signature Foo :: ...
0
votes
1
answer
130
views
Can I use quantifier elimination to get models for 'c' in formulae like ∃a.∀b.∃c.∀d. Phi?
Consider I have a formula with the shape: ∃a.∀b.∃c.∀d. Phi, where a,b,c,d belong to some first-order theory T that admits quantifier elimination.
If I would like to get a model of this formula in Z3, ...
0
votes
1
answer
104
views
What does a model in ∃x∀y∃z∀u . F[x, y, z, u] mean?
In Playing with Quantified Satisfaction they state as follows:
Evaluating a quantified formula of the form ∃x∀y∃z∀u . F[x, y, z, u]
can be naturally seen as a game between two parties: the ...
0
votes
1
answer
176
views
RegEx : Nested Groups and Quantifiers
This is my string : file_1234_test.pdf
Task is to find the filename-without-extension and find the number.
So the result should be :
> Match 1 = file_1234_test.pdf
> Group 1 = file_1234_test
>...
0
votes
0
answers
103
views
Regular expressions, Greek characters and the *-quantifier doesn't work (but the +-quantifier does)?
I use this regular expression [\p{Greek}] to match any Greek character. It works as expected and matches the first Greek character on the line. However, I want to match all Greek characters that ...