Can I use declare-const to eliminate the forall universal quantifier?

Posted by monica on Stack Overflow See other posts from Stack Overflow or by monica
Published on 2012-11-05T23:14:57Z Indexed on 2012/11/07 5:00 UTC
Read the original article Hit count: 284

Filed under:

z3

|

theorem-proving

I have some confusion of using universal quantifier and declare-const without using forall

(set-option :mbqi true)
(declare-fun f (Int Int) Int)
(declare-const a Int)
(declare-const b Int)

(assert (forall ((x Int)) (>= (f x x) (+ x a))))

I can write like this:

(declare-const x Int)
(assert  (>= (f x x) (+ x a))))

with Z3 will explore all the possible values of type Int in this two cases. So what's the difference? Can I really use the declare-const to eliminate the forall quantifier?

© Stack Overflow or respective owner

Related posts about z3

Can I use declare-const to eliminate the forall universal quantifier?

as seen on Stack Overflow - Search for 'Stack Overflow'
I have some confusion of using universal quantifier and declare-const without using forall (set-option :mbqi true) (declare-fun f (Int Int) Int) (declare-const a Int) (declare-const b Int) (assert (forall ((x Int)) (>= (f x x) (+ x a)))) I can write like this: (declare-const x Int) (assert… >>> More
Optimized algorithm for line-sphere intersection in GLSL

as seen on Game Development - Search for 'Game Development'
Well, hello then! I need to find intersection between line and sphere in GLSL. Right now my solution is based on Paul Bourke's page and was ported to GLSL this way: // The line passes through p1 and p2: vec3 p1 = (...); vec3 p2 = (...); // Sphere center is p3, radius is r: vec3 p3 = (...); float… >>> More
curl POST to RESTful services

as seen on Stack Overflow - Search for 'Stack Overflow'
Hello All, There are a lot of questions on Stackoverflow about curl but I could not figure out what is that I am doing what I am not supposed to. I am trying to call a RESTful service that I had written using Jersey API and am trying to POST an xml string to it and I get HTTP 415 error which is supposed… >>> More
joomla SEF shows differrent links in Homepage than inner pages !!

as seen on Stack Overflow - Search for 'Stack Overflow'
I'm enabling Joomla SEF , and get the following results when I link to an article from a homepage (frontpage) article: anywebsite.com/component/content/article/26/141-Z1-Z2-Z3-Z4 but when linking from other articles I get the result I want which is : anywebsite.com/Categor/141-Z1-Z2-Z3-Z4 and… >>> More
Fastest pathfinding for static node matrix

as seen on Game Development - Search for 'Game Development'
I'm programming a route finding routine in VB.NET for an online game I play, and I'm searching for the fastest route finding algorithm for my map type. The game takes place in space, with thousands of solar systems connected by jump gates. The game devs have provided a DB dump containing a list of… >>> More

Related posts about theorem-proving

Project ideas for automated deduction/automated theorem proving?

as seen on Stack Overflow - Search for 'Stack Overflow'
Dear Stack Overflow brethren, I'm a second-semester junior who will embark upon my thesis soon, and I have an interest in automated deduction and automated theorem provers. As in, I'd like to advance the art in some way (I don't mean that pretentiously, but I do want to do something productive)… >>> More
What's your favourite assisted theorem prover?

as seen on Stack Overflow - Search for 'Stack Overflow'
Hi all, I'm hoping to pick one of the many assisted theorem provers (rather than automatic ones) but there are rather a lot to choose from! Does anyone have any you prefer and may I ask why? Thanks! >>> More
Can I use declare-const to eliminate the forall universal quantifier?

as seen on Stack Overflow - Search for 'Stack Overflow'
I have some confusion of using universal quantifier and declare-const without using forall (set-option :mbqi true) (declare-fun f (Int Int) Int) (declare-const a Int) (declare-const b Int) (assert (forall ((x Int)) (>= (f x x) (+ x a)))) I can write like this: (declare-const x Int) (assert… >>> More
A Taxonomy of Numerical Methods v1

as seen on Geeks with Blogs - Search for 'Geeks with Blogs'
Numerical Analysis – When, What, (but not how) Once you understand the Math & know C++, Numerical Methods are basically blocks of iterative & conditional math code. I found the real trick was seeing the forest for the trees – knowing which method to use for which situation. Its pretty easy… >>> More