#
a229f91c |
|
26-Jun-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Use Unicode quotes in some self-test output
|
#
1c653e3e |
|
06-Feb-2017 |
Thomas Tuerk <thomas@tuerk-brechen.de> |
implement simple quantifier heuristics The quantifier heuristics library is powerful, but often slow. The unwind conversions are fast, but have serious restrictions. This commits adds simple quantifier heuristics. They are based on the techniques developed for quantifier heuristics library, but only search gap guesses that don't contain free variables. Some very limited experiments suggest that it is similarly fast as unwind. It can handle all the cases unwind can handle. However, it supports also a much richer syntax. Moreover, it can instantiate in addition to universal and existential quantifiers also unique existential quantifiers, eliminate select and some. Moreover, it knows about pairs and lists.
|
#
136e6cb0 |
|
29-Aug-2015 |
Thomas Tuerk <thomas@tuerk-brechen.de> |
fix selftest of quantHeuristicsLib The recent changes to how context is processed were unluckily not propagated to the selftests. This fixes the resulting errors.
|
#
8d315d0c |
|
09-Dec-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
Delete trailing whitespace in src/ This needs doing periodically, and is best done to a whole bunch of files at once.
|
#
08d7a558 |
|
23-Oct-2014 |
Piotr Trojanek <piotr.trojanek@gmail.com> |
trailing newlines in *.{sml,sig} files from src/ removed Trailing newlines from SML files in src/ were rendered in HTML documentation.
|
#
b34caa6e |
|
08-Aug-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
Fix quantHeuristics selftest to cope with change in cd00950
|
#
9b9370ac |
|
17-Oct-2012 |
Thomas Tuerk <tt291@cl.cam.ac.uk> |
quantifierHeuristics tweaks - some tweaks to make sum_qp behave nicer - for this some small changes that can be seen as bug fixes or minor feature improvements
|
#
00891b6f |
|
11-Oct-2012 |
Thomas Tuerk <tt291@cl.cam.ac.uk> |
quantHeuristicsLib bug fixes - back-chaining only applied weakening, if a rule could be applied for both threngthening and weakening - trouble with free type-variable clashes fixed
|
#
43f15686 |
|
02-Oct-2012 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Delete trailing whitespace in src/
|
#
5854343a |
|
21-Sep-2012 |
Thomas Tuerk <tt291@cl.cam.ac.uk> |
bug-fix in Sanity.sml another cleanup of quantHeuristicsLib
|
#
b0d02af8 |
|
18-Sep-2012 |
Thomas Tuerk <tt291@cl.cam.ac.uk> |
extended interface for quantifier heuristics Now additional context as well as lemmata used for weakening / strengthening can be added to quantifier heuristic parameters.
|
#
68865120 |
|
11-Sep-2012 |
Thomas Tuerk <tt291@cl.cam.ac.uk> |
Added support for context to quantifier heuristics, add sum_qp
|
#
4480c57d |
|
24-Aug-2012 |
Thomas Tuerk <tt291@cl.cam.ac.uk> |
cleanup of quantifier heuristics library - more sensible names for guesses - quantHeuristicsLib renamed to quantHeuristicsLibBase - quantHeuristicsLibArgs renamed to quantHeuristicsLibParameters - new shorter signature defined in quantHeuristicsLib - adaptation of usage of quantHeuristicsLib
|
#
d7a852e2 |
|
31-Jul-2012 |
Thomas Tuerk <tt291@cl.cam.ac.uk> |
More on quantfier heuristics (I did not add all changes to the first commit)
|
#
845531b5 |
|
14-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove trailing whitespace in source files.
|
#
deec6b4e |
|
26-Oct-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
fix problem in selftest with standard-kernel
|
#
f0f0804c |
|
26-Oct-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
fixed a minor bug with free vars in quantHeuristicsLib, selftest now terminates when encountering a problem
|
#
e09c9510 |
|
18-Sep-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
- reimplementation of quantHeuristicsLib. - move parts of quantHeuristicsLib to quantHeuristicsTools - selftest added Before guesses were justified by hand crafted theorems. There were modified using low level forward proof techniques. This resulted in quantHeuristicsLib being hard to understand and maintain. This reimplementation exploits recent addition to pairTools about handling paired quantification in order to introduce general predicates for guess theorems. Defining special predicates allows proving general lemmata easily. quantHeuristicsLib can the use the lemmata instead of low level proofs. However, this comes with the additional cost of introducing and eliminating tupled quantifiers. The new version is easier to understand and maintain. Moreover, it became much simpler to add user specified heuristics. The behavior changed slightly. For example, unnecessary priming of newly introduced variables has been eliminated.
|