summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip

aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"

move stronger rules into exercise

added a function that carries out all the reconstruction steps, for improved usability;
added documentation;

reconstruction framework for LEO-II's TPTP proofs;

made list of test files a parameter to timed_test in TPTP_Test.thy, and updated dependent definitions;

cleaned code used to produce a proof-graph;

improved configurability of DOT exporter;
tuned;

behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
tuned;

experimented with presentation of DOT+LaTeX;

edges are now being shown in the proof graph;
removed the shapes related to the conjecture and the negated conjecture, to remove clutter (since i'm also showing the inference's conclusion in latex);