setting up Code_Prolog_Examples

adding queens and symbolic derivation example for prolog code generation

adding parsing of numbers; improving output of solution without free variables in prolog code generation

adding preprocessing of introduction rules to replace the constant Predicate.eq in the prolog code generation

adding basic arithmetic support for prolog code generation

adding numbers as basic term in prolog code generation

More consistent naming of locale api functions.

Documentation of 'interpret' updated.

print_interps shows interpretations in proofs.

Interpretation in proofs supports mixins.

Make registrations generic data.

merged

don't choke on synonyms when parsing SPASS's Flotter output + renamings; the output format isn't documented so it was hard to guess that a single clause could be associated with several names...

fix Mirabelle timeout

make Mirabelle happy

fix bug in the newly introduced "bound concealing" code

handle division by zero gracefully (used to raise Unordered later on)

use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures; this replaces the previous, somewhat messy solution of adding "extra" clauses

fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)

handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs

revert exception throwing in FOL_SOLVE, since they're not caught anyway

avoid "ATP Error: Error: blah" style messages

avoid "_def_raw" theorems

better error and minimizer output

deal with chained facts more gracefully

speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"

work around atomization failures

fiddle with the fudge factors, to get similar results as before

perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs

fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)

generate correct names for "$true" and "$false"; this was lost somewhere in the non-clausification

don't assume canonical rule format

avoid "clause" and "cnf" terminology where it no longer makes sense

"axiom_clauses" -> "axioms" (these are no longer clauses)

remove the "extra_clauses" business introduced in 19a5f1c8a844; it isn't working reliably because of: * relevance_override * it is ignored anyway by TPTP generator A better solution would/will be to ensure monotonicity: extra axioms not used in an ATP proof shouldn't make the rest of the problem provable

adapting output for first solution

removing pointless type information in internal prolog terms

cleaning example file; more natural ordering of variable names

improving translation to prolog; restoring terms from prolog output; adding tracing support

working on parser for prolog reponse

querying for multiple solutions in values command for prolog execution

correcting scanning

adding values command and parsing prolog output

adding example file for prolog code generation; adding prolog code generation example to IsaMakefile

adding a mockup version for prolog code generation

exporting retrieval function for graph of introduction rules in the predicate compiler core

merged

rebinding ref is illegal

tuned example

intermediate operation avoids invariance problem in Scala

merged

kill polymorphic "val"s

improved ATP error handling some more

shorter URL

mention version numbers

fiddled with usage text

handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on

merged

tuned printing of applications and let cascades

checking Scala_imp