Loading...
Please wait, while we are loading the content...
Similar Documents
Mechanized quantifier elimination for linear real-arithmetic in Isabelle / HOL
| Content Provider | Semantic Scholar |
|---|---|
| Author | Chaieb, Amine |
| Copyright Year | 2006 |
| Abstract | We integrate Ferrante and Rackoff's quantifier elimination procedure for linear real arithmetic in Isabelle/HOL in two manners: (a) tactic-style, i.e. for every problem instance a proof is generated by invoking a series of inference rules, and (b) reflection, where the whole algorithm is implemented and verified within Isabelle/HOL. We discuss the performance obtained for both integrations. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www4.in.tum.de/~chaieb/pubs/pdf/ferrack.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |