Email Gateway (Aug 18 2022 at 13:38): Email Gateway (Aug 18 2022 at 13:38):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
Hello,
I'm wondering about the decision procedures present in Isabelle - which
ones have been implemented.
In particular, I am considering implementing some, probably based on
term normalisation, and then trying to automatically find bijective
mappings between theories in progress and those to which known decision
procedures apply. Any comments and suggestions on existing work in
Isabelle (or other systems) is most welcome.
thanks,
lucas
Email Gateway (Aug 18 2022 at 13:39):From: Amine Chaieb <ac638@cam.ac.uk>
Dear Lucas,
Here are the decision procedures I know of in Isabelle. There are surely
more, which are not related to arithmetic.
1) First-order formulas (semi-decision) --- This is early work by Larry
Paulson and "recent" work by Joe Hurd. Of course they are available in
all HOL families.
2) Fourrier-Motzkin method for linear arithmetic. This is also available
in all HOL Families and as far as I heard also in Coq (maybe an other
algorithm Omega by Pugh which works for integers). Typically it proves
universal theorems over linear real arithmetic, but it can be very
easily changed to prove theorems over the integers (and consequently
natural numbers). This is also available in Isabelle and HOL Light (I
guess in HOL4 too).
3) Quantifier elimination for linear integer arithmetic (Presburger
Arithmetic). This is available in Isabelle/HOL, HOL Light and HOL 4
4) Quantifier elimination for Tarski-algebra (Real numbers with plus and
times and ordering). This is available in HOL Light and in HOL (88?).
Not yet in Isabelle, but there is some work going on.
5) Quantifier elimination for the complex numbers. This is available in
HOL Light and I have also ported it to Isabelle/HOL but never found its
way in to the distribution, because it was quite slow on interesting
examples and there was no real applications.
6) Quantifier elimination for Dense linear orders. This is available in
Isabelle/HOL (Maybe in other HOL families --- but is really too simple
to be worth mentioning).
7) Quantifier elimination for linear real arithmetic. This is available
in Isabelle/HOL (the algorithm of Ferrante Rackoff and if you do some
transformations you can apply a Variant of Loos Weispfenning formalized
by Tobias Nipkow).
There is also a version where you are allowed to multiply quantifier
variables with non-linear parameters.
All theses apply to any ordered zero-totalized field (and hence for the
real numbers are a subclass of Tarski-algebra).
8) Universal inequalities over the real numbers --- Using sums of
squares and semidefinite programming. This is available in HOL Light and
has also been ported to Isabelle/HOL. Laurent Thery also ported two
years (or so) ago to Coq.
9) Universal equalities in Rings (using Groebner Bases). This is
available in HOL Light and Isabelle. The extension to an interesting
forall-exists fragment for ring-equalities is also available in both
systems. In Coq there is a very basic version of this which tells you OK
if two ring terms are equal (without using assumptions).
10) Quantifier elimination for mixed linear-real arithmetic (using the
floor-function). This is available in Isabelle/HOL. I am not aware of
any other theorem prover having this decision procedure.
11) There is also a formalization of DPLL (T) and SAT by Filip Maric and
Predrag Janicic in Isabelle/HOL
Hope it helps,
Amine.
You might be interested in glancing at the following paper which
addresses the issue of writing proof-method which work under
interpretation of locales --- i.e. apply to several structures at once:
Amine Chaieb and Makarius Wenzel. Context aware Calculation and
Deduction - Ring Equalities via Gröbner Bases in Isabelle. In M. Kauers,
M. Kerber, R. Miner, and W. Windsteiger, editors, / CALCULEMUS 2007/,
volume 4573 of /Lecture Notes in Computer Science/, pages 27-39.
Springer, 2007. [ bib
<http://www4.in.tum.de/%7Echaieb/pubs/pubs_bib.html#Chaieb-Wenzel:2007a> |
.pdf <http://www4.in.tum.de/%7Echaieb/pubs/pdf/morphism.pdf> ]
Email Gateway (Aug 18 2022 at 13:40):From: Michael Norrish <Michael.Norrish@nicta.com.au>
Amine Chaieb wrote:
I believe the "Omega" implemented in Coq is just F-M elimination (and
thus incomplete for the integers). This was the case a few years ago.
The full Omega is implemented in HOL4, and is a quantifier elimination
procedure for Presburger arithmetic over the integers. I recommend
its implementation if you're looking for something to do in Isabelle:
it performs better than Cooper's algorithm on many typical problems.
(There are also other problems where Cooper's is better.)
Michael.
Last updated: May 03 2024 at 04:19 UTC