e9458b1a7a19a63aa4c179f9ab20f4d50681c168 |
|
25-Mar-2016 |
Jens Elkner <jel+git@iws.cs.uni-magdeburg.de> |
applied utils/replaceAllHeaders.sh
- all $Header$ tokens in doc comments replaced with corresponding filename |
cddd87cd39be9d031348ef95051c4d14067e1646 |
|
22-Oct-2014 |
cmaeder <cmaeder@users.noreply.github.com> |
use usable provers and cons-checkers |
11c3a215d5cf043181e83929f1ce214df65cb587 |
|
18-Dec-2013 |
Christian Maeder <Christian.Maeder@dfki.de> |
show lib-ids without ankle brackets
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18401 cec4b9c1-7d33-0410-9eda-942365e851bb |
3d3889e0cefcdce9b3f43c53aaa201943ac2e895 |
|
29-Nov-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
removed lots of hlint warnings
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18342 cec4b9c1-7d33-0410-9eda-942365e851bb |
c5f9e2f0598f061c50c7f097add808c0ec7d1fea |
|
31-Jul-2013 |
Loredana Mihaela Diaconu <lo.diaconu@jacobs-university.de> |
866 with correct time limit
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18108 cec4b9c1-7d33-0410-9eda-942365e851bb |
4eefbf3ad21b510729d5423d08de513b310e9cd0 |
|
31-Jul-2013 |
Loredana Mihaela Diaconu <lo.diaconu@jacobs-university.de> |
866
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18103 cec4b9c1-7d33-0410-9eda-942365e851bb |
42f76486938cb03ba650ee09c68304fd4a86fb87 |
|
28-Jul-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
command show-comorphisms-to for interactive console
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18072 cec4b9c1-7d33-0410-9eda-942365e851bb |
46b5fe38c0c8cd7b8a92ccb44e683e4996aea19c |
|
24-Jul-2013 |
Loredana Mihaela Diaconu <lo.diaconu@jacobs-university.de> |
attempt at 866
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18053 cec4b9c1-7d33-0410-9eda-942365e851bb |
1caac17e785f1133f7c4d9a97f367f7832823cfc |
|
27-Mar-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
* fixed a bug in Common.GraphAlgo.yen (first node in a path can be the spur node too)
* removed debug output
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17833 cec4b9c1-7d33-0410-9eda-942365e851bb |
247eefa106a467b872521724ff7bf4af5c27220d |
|
27-Mar-2013 |
Jonathan von Schroeder <sternkinder@gmail.com> |
new detection of comorphisms to provers
todo: investigate why found provers do not show up (example THF/Test/Products.hascasl)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17830 cec4b9c1-7d33-0410-9eda-942365e851bb |
5607bbe40d1b360797381a83a6eae6773ee7cd2c |
|
27-Jan-2011 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored abstract proof state
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@14435 cec4b9c1-7d33-0410-9eda-942365e851bb |
dba73947b1f8befd8ffb81fbed7deb6e582f3f62 |
|
27-Jan-2011 |
Christian Maeder <Christian.Maeder@dfki.de> |
wrap up free def links
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@14430 cec4b9c1-7d33-0410-9eda-942365e851bb |
52e3fbd71a34c294b93a44c02829991e044d163b |
|
07-Jan-2011 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored getting provers
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@14354 cec4b9c1-7d33-0410-9eda-942365e851bb |
8969a00d3fa8a33b08c85afd50ab675a56ee6f84 |
|
07-Jan-2011 |
Christian Maeder <Christian.Maeder@dfki.de> |
moved filter hasModelExpansion to getProvers
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@14353 cec4b9c1-7d33-0410-9eda-942365e851bb |
abee46762c1663b85c6f18d934cd11df83828f6e |
|
07-Jan-2011 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed GetPName class
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@14349 cec4b9c1-7d33-0410-9eda-942365e851bb |
325e8aca700ad30d8ac47a00482c02dea2de3df0 |
|
24-Sep-2010 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed disprove button to be put into the node menu
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@14092 cec4b9c1-7d33-0410-9eda-942365e851bb |
98890889ffb2e8f6f722b00e265a211f13b5a861 |
|
01-Sep-2010 |
Corneliu-Claudiu Prodescu <Corneliu-Claudiu.Prodescu@dfki.de> |
Added see license.txt to license field
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13959 cec4b9c1-7d33-0410-9eda-942365e851bb |
b87efd3db0d2dc41615ea28669faf80fc1b48d56 |
|
11-Aug-2010 |
Corneliu-Claudiu Prodescu <Corneliu-Claudiu.Prodescu@dfki.de> |
Changed haddock headers and inserted empty headers for the ones missing
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13857 cec4b9c1-7d33-0410-9eda-942365e851bb |
1036463e0cb9fff54e4f9378bdf2face4bb58bc4 |
|
22-Jul-2010 |
Simon Ulbricht <tekknix@informatik.uni-bremen.de> |
added 'LNode DGNodeLab' as input parameter to ProverGUI and GtkProverGUI
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13749 cec4b9c1-7d33-0410-9eda-942365e851bb |
158e6d8b5f7ebabef2d020ff045ede18fab15ff9 |
|
20-Jul-2010 |
Christian Maeder <Christian.Maeder@dfki.de> |
splitted up Proofs/InferBasic.hs
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13732 cec4b9c1-7d33-0410-9eda-942365e851bb |
1937dccb04b363364f7a7de17fdaae1d70583af9 |
|
15-Jul-2010 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored global theory results
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13718 cec4b9c1-7d33-0410-9eda-942365e851bb |
c2b17498cf4334382500475dc0f5556264e52079 |
|
26-May-2010 |
Christian Maeder <Christian.Maeder@dfki.de> |
new lemmas also need proofs
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13443 cec4b9c1-7d33-0410-9eda-942365e851bb |
06799f39787bc3facfaebb50bdc87439d2b6f99b |
|
26-May-2010 |
Christian Maeder <Christian.Maeder@dfki.de> |
added new lemmas #793 to prove GUI
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13439 cec4b9c1-7d33-0410-9eda-942365e851bb |
95b3cfab4eca1e97bf707e88684c80afb1ab3b94 |
|
02-Feb-2010 |
Christian Maeder <Christian.Maeder@dfki.de> |
improved model reconstruction
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13021 cec4b9c1-7d33-0410-9eda-942365e851bb |
29d0028b733c2c9b909095ed1eb397131c910daf |
|
28-Jan-2010 |
Christian Maeder <Christian.Maeder@dfki.de> |
reverted spechub/Hets@efbd7d8430586d839626c43c7ec93cc508140992 #778
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13012 cec4b9c1-7d33-0410-9eda-942365e851bb |
efbd7d8430586d839626c43c7ec93cc508140992 |
|
28-Jan-2010 |
Christian Maeder <Christian.Maeder@dfki.de> |
added original sentences to extracted model
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13010 cec4b9c1-7d33-0410-9eda-942365e851bb |
8fb30a9b125280ae8910352580b94de9a7863a24 |
|
05-Jan-2010 |
Christian Maeder <Christian.Maeder@dfki.de> |
added argument to include theorems in consistency checker
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12967 cec4b9c1-7d33-0410-9eda-942365e851bb |
feb4e4217d5621a971077c8399b4b49237f07bac |
|
23-Dec-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12957 cec4b9c1-7d33-0410-9eda-942365e851bb |
2d00b580613fcdc777040a3f855e5cdbdac5d8df |
|
22-Dec-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed warnings (detected by ghc-6.12.1)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12953 cec4b9c1-7d33-0410-9eda-942365e851bb |
8757ec521b14e710ff664a39993b6b10f3468d5b |
|
14-Dec-2009 |
Thiemo Wiedemeyer <raider@informatik.uni-bremen.de> |
Goal list in prover windows and node list in consistency checker are sortet by status and name. see #323
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12927 cec4b9c1-7d33-0410-9eda-942365e851bb |
0cdeccb66730b876f73bddd2705ddc62e180320d |
|
10-Dec-2009 |
Thiemo Wiedemeyer <raider@informatik.uni-bremen.de> |
Removed consistency check node menu button. Removed duplicated code from InferBasic.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12909 cec4b9c1-7d33-0410-9eda-942365e851bb |
90fbaf1cd73486129e26e1ac94a413550832e4d6 |
|
07-Dec-2009 |
Thiemo Wiedemeyer <raider@informatik.uni-bremen.de> |
fixed timeout issue.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12897 cec4b9c1-7d33-0410-9eda-942365e851bb |
a18015595fd0b82e9315287abf98a9590f18522d |
|
03-Dec-2009 |
Thiemo Wiedemeyer <raider@informatik.uni-bremen.de> |
filtered nodes with empty theory. these nodes are shown in result window as consistent but are not availible as goal. added timeout function to inferbasic for checkers without own timeout handling.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12891 cec4b9c1-7d33-0410-9eda-942365e851bb |
f7b9d64160c23654b7288a3b0ee3e2b95af3e752 |
|
15-Nov-2009 |
Thiemo Wiedemeyer <raider@informatik.uni-bremen.de> |
fixed deadlock bug in GtkProverGUI. removed GUIMVar from GInfo, because it is not needed.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12836 cec4b9c1-7d33-0410-9eda-942365e851bb |
80c2d23821d095b55d9a547f48fc3fcdc27df405 |
|
28-Oct-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored consistency checkers
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12745 cec4b9c1-7d33-0410-9eda-942365e851bb |
3a6decfd748f532d5cb03fbcb7a42fa37b0faab3 |
|
16-Oct-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored prover stuff
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12661 cec4b9c1-7d33-0410-9eda-942365e851bb |
c854d07f4a300570baeb9763ab8820e163e1827f |
|
15-Oct-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
slightly improve cons-checker output (needs more work)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12649 cec4b9c1-7d33-0410-9eda-942365e851bb |
c936954e92d5ce1f0f68f0a5224a5925fca88d6b |
|
13-Oct-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
report consistency although model reconstruction failed
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12637 cec4b9c1-7d33-0410-9eda-942365e851bb |
ad6a71bc29879c37f9bb43a20761bc102147ed31 |
|
12-Oct-2009 |
Thiemo Wiedemeyer <raider@informatik.uni-bremen.de> |
timeout does now work for consistency checker. also moved comSublogics to Grothendieck and named it joinSublogics.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12632 cec4b9c1-7d33-0410-9eda-942365e851bb |
ec25781c1180ea07f66b48c34f93cf5634e9277c |
|
07-Oct-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
moved ComputeTheory to folder Static
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12587 cec4b9c1-7d33-0410-9eda-942365e851bb |
96d23995ee55ff3af632eedbb9e7ffc293a414a2 |
|
05-Oct-2009 |
Thiemo Wiedemeyer <raider@informatik.uni-bremen.de> |
added analysis of results to consistencyCheck.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12575 cec4b9c1-7d33-0410-9eda-942365e851bb |
e7d2b3903c7b44db432538b0d720c21062c24823 |
|
26-Sep-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
hlinted
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12526 cec4b9c1-7d33-0410-9eda-942365e851bb |
e49fd57c63845c7806860a9736ad09f6d44dbaed |
|
23-Sep-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored, camel cased, library names
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12493 cec4b9c1-7d33-0410-9eda-942365e851bb |
8c4cc09642696141694f9c3f1f2838f6c0b184a0 |
|
10-Sep-2009 |
Thiemo Wiedemeyer <raider@informatik.uni-bremen.de> |
added more functionality to consistancy checker gui. node and finder selection is now working.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12454 cec4b9c1-7d33-0410-9eda-942365e851bb |
62f38a562115f39afdec71801ba3b74d53706db7 |
|
07-Sep-2009 |
Thiemo Wiedemeyer <raider@informatik.uni-bremen.de> |
added pulsebar. #699
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12429 cec4b9c1-7d33-0410-9eda-942365e851bb |
8f31d51d47da96200437dd3af1d785cd88a46f71 |
|
13-Aug-2009 |
Thiemo Wiedemeyer <raider@informatik.uni-bremen.de> |
added skeleton for a gtk version of the prover window.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12116 cec4b9c1-7d33-0410-9eda-942365e851bb |
1780ec6fd307212ae6834d85ae6b5d38e059c444 |
|
20-Jul-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
splitted ComputeTheory from TheoremHideShift
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11976 cec4b9c1-7d33-0410-9eda-942365e851bb |
d7089fd155d01e2a427f7461bd16bb325585eb18 |
|
16-Jul-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
an empty theory can be handled by darwin if at least one true axiom is generated
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11954 cec4b9c1-7d33-0410-9eda-942365e851bb |
ce1c76a52a42788c085b7794a1a5f9758799a0e2 |
|
08-May-2009 |
Markus Gross <Markus.Gross@dfki.de> |
Removed CommandHistory and refactored proof-history handling. Fixes #690
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11762 cec4b9c1-7d33-0410-9eda-942365e851bb |
e9f663929f8c759b07f6629e77c78b14013408c0 |
|
27-Mar-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
check empty theory before consistency
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11616 cec4b9c1-7d33-0410-9eda-942365e851bb |
95cb954c00f873306bf1a60b62d3209d3cff4102 |
|
27-Mar-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored runProveAtNode and basic inference
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11611 cec4b9c1-7d33-0410-9eda-942365e851bb |
2ff9b0bc8bcec5a8c39c9288eb2ae43b9ab6d3f6 |
|
26-Mar-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
wibble
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11602 cec4b9c1-7d33-0410-9eda-942365e851bb |
1e3aca4178372af672efb237d16087c603fe5564 |
|
26-Mar-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
call "Prove Structured" via proofMenu rather than via proveAtNode and basicInferenceNode
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11596 cec4b9c1-7d33-0410-9eda-942365e851bb |
6c08e47c4275556c18f4f89521bf21fe94c28dd5 |
|
18-Mar-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored or reverted computeTheory
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11544 cec4b9c1-7d33-0410-9eda-942365e851bb |
dada658692dfbbd04b7a08cdc4826616f84ad6ef |
|
26-Feb-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
support unguarded inclusion
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11441 cec4b9c1-7d33-0410-9eda-942365e851bb |
1ac36418f204bbe56f4cd951a979180721758999 |
|
19-Jan-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
extended for structured VSE proofs
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11281 cec4b9c1-7d33-0410-9eda-942365e851bb |
8f5219469b89a15dc6d4c2c30463775975f5841c |
|
15-Jan-2009 |
Razvan Pascanu <r.pascanu@jacobs-university.de> |
history issue fixed
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11265 cec4b9c1-7d33-0410-9eda-942365e851bb |
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5 |
|
15-Jan-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed trailing spaces
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11264 cec4b9c1-7d33-0410-9eda-942365e851bb |
71654489020a03cf6ce9f2947f3da26a996f9c32 |
|
07-Jan-2009 |
Razvan Pascanu <r.pascanu@jacobs-university.de> |
Changes to GUI to use common datatypes in Interfaces
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11229 cec4b9c1-7d33-0410-9eda-942365e851bb |
8244e8866cad2be73b7e2b76a6659535f0f728cc |
|
28-Nov-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
report goal status
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11117 cec4b9c1-7d33-0410-9eda-942365e851bb |
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7 |
|
25-Nov-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed trailing spaces
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11082 cec4b9c1-7d33-0410-9eda-942365e851bb |
8ca41bee48c7322dbaa5ac27328836b3d15b3d8f |
|
24-Nov-2008 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
more friendly treatment of missing freedefs
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11075 cec4b9c1-7d33-0410-9eda-942365e851bb |
ad69cb3627839ed3d33f13d71c81378b65a24b35 |
|
24-Nov-2008 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
added theory to FreeDefMorphism
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11064 cec4b9c1-7d33-0410-9eda-942365e851bb |
5cf0f23d6436a66629796c8d5b67698571dde55e |
|
19-Nov-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
consider free and cofree def-links #615
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11039 cec4b9c1-7d33-0410-9eda-942365e851bb |
999f839e42d594e4ae288208fec398626837c41c |
|
19-Nov-2008 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
completed handling of free definition links, see ticket #563
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11037 cec4b9c1-7d33-0410-9eda-942365e851bb |
594891d02ecf595cd5fdd12e8036e686f1b90ddf |
|
18-Nov-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
computed free definition links for provers #613
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11029 cec4b9c1-7d33-0410-9eda-942365e851bb |
b4deba573a8057214f2d18512ba0a948c26d5582 |
|
18-Nov-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored thName computation
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11026 cec4b9c1-7d33-0410-9eda-942365e851bb |
4b136ad539bd9f4e115dff4eee4d552a42d4437e |
|
14-Nov-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored proof history #601
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11015 cec4b9c1-7d33-0410-9eda-942365e851bb |
f094a7999dfa79cad2eb34ce15f1939c0d6b9e39 |
|
14-Nov-2008 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
refactored prover interface: carry around freeness constraints
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11008 cec4b9c1-7d33-0410-9eda-942365e851bb |
433bb7cb49200f4e6c7341101da25309e423c0e2 |
|
14-Nov-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored prover template
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11005 cec4b9c1-7d33-0410-9eda-942365e851bb |
b67b0e660972500608206ec05cb128b1c68e8909 |
|
09-Oct-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed conflict junk
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10797 cec4b9c1-7d33-0410-9eda-942365e851bb |
522e92d98ffff311567afdfce0530f86dcf164ab |
|
08-Oct-2008 |
Igor Stassiy <i.stassiy@jacobs-university.de> |
Importing of Static.DGFlattening is not neccessary here, changes the
name of function singleTree_flattening_dunions.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10791 cec4b9c1-7d33-0410-9eda-942365e851bb |
f2dbbb3cadb29d9d7603b8413040f25fc5087b43 |
|
01-Oct-2008 |
Markus Gross <Markus.Gross@dfki.de> |
Introduced datastructures for history commands; Saving the history will convert the commands to strings; Bug fixes
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10761 cec4b9c1-7d33-0410-9eda-942365e851bb |
d5fe06af711a6912ae028ebf873eada4ee8733f8 |
|
23-Sep-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
replaced umlaut in Luettich
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10718 cec4b9c1-7d33-0410-9eda-942365e851bb |
697e63e30aa3c309a1ef1f9357745111f8dfc5a9 |
|
22-Sep-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
separated library names from HetCASL libraries
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10708 cec4b9c1-7d33-0410-9eda-942365e851bb |
0e4d6088b64f4d2a4bf2b4755a0d187de6c2bb59 |
|
19-Sep-2008 |
Markus Gross <Markus.Gross@dfki.de> |
better statement
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10697 cec4b9c1-7d33-0410-9eda-942365e851bb |
6e5dd768c75903bf57407ac03f50550bcd9fdd92 |
|
19-Sep-2008 |
Markus Gross <Markus.Gross@dfki.de> |
better statement
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10696 cec4b9c1-7d33-0410-9eda-942365e851bb |
f9aa644af131a2571514a7e5bbd8901e32ad6273 |
|
19-Sep-2008 |
Markus Gross <Markus.Gross@dfki.de> |
now processing proof-trees directly and adding only proven goals
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10695 cec4b9c1-7d33-0410-9eda-942365e851bb |
16cef01b8c0a4ecd453efadd5a03134cfff62baf |
|
01-Sep-2008 |
Markus Gross <Markus.Gross@dfki.de> |
The development graph now generates tactic script information which can be saved via the menu item: Edit -> Save proof-script.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10620 cec4b9c1-7d33-0410-9eda-942365e851bb |
e533f73a960250a92de4d3aab3b608d8b8ca7af3 |
|
25-Aug-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed unused imports
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10582 cec4b9c1-7d33-0410-9eda-942365e851bb |
df75389b9266b115f0dc71a97679aec3dc0e48e1 |
|
22-Aug-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
lifting failure is unnecessary
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10579 cec4b9c1-7d33-0410-9eda-942365e851bb |
dd5e505efb3641bf74ade0ba3adabf4ceaf94e60 |
|
01-Aug-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed trailing blank lines
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10427 cec4b9c1-7d33-0410-9eda-942365e851bb |
ec980efaa0ef669b0a999d69c87e32edd1b5e54d |
|
17-Jul-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
extended prover template to accept imports
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10348 cec4b9c1-7d33-0410-9eda-942365e851bb |
038fc609b1d0dfe9698c4cab26fc7db2225820ef |
|
23-Jun-2008 |
Mihai Codescu <mcodescu@informatik.uni-bremen.de> |
introduced flag for computeTheory to use normal forms just when possible
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10179 cec4b9c1-7d33-0410-9eda-942365e851bb |
36f69d35e01d2d6b6bdc165b49661f2a80af8687 |
|
11-Jun-2008 |
Mihai Codescu <mcodescu@informatik.uni-bremen.de> |
computeTheory and theoremHideShift changes
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10088 cec4b9c1-7d33-0410-9eda-942365e851bb |
9b4526ad3c7428b8c3c0ad9ee5d8268acdeee606 |
|
09-May-2008 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
checked model expansiveness also when recomputing fine grained selection
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9999 cec4b9c1-7d33-0410-9eda-942365e851bb |
a975722baf6fee1ca3e67df170c732c4abd0a945 |
|
22-Apr-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
let extractModel return a new signature
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9955 cec4b9c1-7d33-0410-9eda-942365e851bb |
209f37a7f7b3c61e5dc1a90bd83b65a24c8be3fa |
|
22-Apr-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
check goalStatus before extracting model
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9953 cec4b9c1-7d33-0410-9eda-942365e851bb |
63324a97283728a30932828a612c7b0b0f687624 |
|
21-Apr-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
prepare model computation
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9947 cec4b9c1-7d33-0410-9eda-942365e851bb |
afe76697dd6888856a066934a1112a38809b27fa |
|
27-Mar-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
used mapAccumL to collect changes
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9843 cec4b9c1-7d33-0410-9eda-942365e851bb |
cc77993cd3db08f4d731a3c218c2a03b547b8da8 |
|
10-Mar-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
replaced almost duplicate LocalInference with Borrowing
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9728 cec4b9c1-7d33-0410-9eda-942365e851bb |
5efed683fd173e9d53bd5f1929ba5b0c8a228710 |
|
11-Feb-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
used labDG instead of safeContextDG
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9542 cec4b9c1-7d33-0410-9eda-942365e851bb |
fdf94376fa12e6f685f87741be2f3d02e03c429e |
|
13-Dec-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
properly computed targetSublogic for a theory
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9364 cec4b9c1-7d33-0410-9eda-942365e851bb |
f9e0b18852b238ddb649d341194e05d7200d1bbe |
|
29-Oct-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
extended signatures are already needed during logic specific static analysis
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9093 cec4b9c1-7d33-0410-9eda-942365e851bb |
1bc5dccbf0083a620ae1181c717fea75e4af5e5c |
|
18-Oct-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
added extended signatures
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9060 cec4b9c1-7d33-0410-9eda-942365e851bb |
17d4f8c5576d93f36cafe68161cdb960ec49ce7c |
|
09-Oct-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
moved ref info deeper into the node label
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9009 cec4b9c1-7d33-0410-9eda-942365e851bb |
da955132262baab309a50fdffe228c9efe68251d |
|
27-Sep-2007 |
Cui Jian <ken@informatik.uni-bremen.de> |
cleaned up codes
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8947 cec4b9c1-7d33-0410-9eda-942365e851bb |
64325303fc09fc4d88ced49be11ff2d29966422a |
|
27-Sep-2007 |
Cui Jian <ken@informatik.uni-bremen.de> |
cleaned up codes
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8938 cec4b9c1-7d33-0410-9eda-942365e851bb |
5674a959750ec9b9290a34317e6de57bcbd3ac01 |
|
24-Sep-2007 |
Cui Jian <ken@informatik.uni-bremen.de> |
added comments
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8896 cec4b9c1-7d33-0410-9eda-942365e851bb |
2eeec5240b424984e3ee26296da1eeab6c6d739e |
|
23-Aug-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
replaced @tzi with @informatik.uni-bremen
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8698 cec4b9c1-7d33-0410-9eda-942365e851bb |
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5 |
|
15-Aug-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
made a separate module for G_theory
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8618 cec4b9c1-7d33-0410-9eda-942365e851bb |
99634745e86bb1c79da4e2b376e580f65ee67082 |
|
25-Jul-2007 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
changed maintainers; improved efficiency of Proofs.BatchProcessing; improved documentation; improved test program
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8475 cec4b9c1-7d33-0410-9eda-942365e851bb |
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0 |
|
28-Jun-2007 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
Generalisation of functions in Proofs.InferBasic for the usage by the
CMDL interface PGIP. It involved renaming of Proofs/GUIState.hs.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8179 cec4b9c1-7d33-0410-9eda-942365e851bb |
cd6e5706893519bfcf24539afa252fcbed5097dd |
|
26-Jun-2007 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
* Refactoring of classes Logic, Sentences and StaticAnalysis
* Logic.Prover.ProverTemplate has now a field for the maximal sublogic
needed by a Prover/ConsChecker
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8145 cec4b9c1-7d33-0410-9eda-942365e851bb |
36acdac14e0ba2a0c5e9d89e93914d7037c42683 |
|
12-Jun-2007 |
Razvan Pascanu <r.pascanu@jacobs-university.de> |
new version of the CMDL interface
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8019 cec4b9c1-7d33-0410-9eda-942365e851bb |
edd35c6c970fa1707dc6ad7a3ba26119e0046223 |
|
30-May-2007 |
Cui Jian <ken@informatik.uni-bremen.de> |
step one of abstraction of DGraph, see ticket 269
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7947 cec4b9c1-7d33-0410-9eda-942365e851bb |
f2c050360525df494e6115073b0edc4c443a847c |
|
12-Apr-2007 |
Mihai Codescu <mcodescu@informatik.uni-bremen.de> |
flags for properties of comorphisms and values for them in different instances
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7813 cec4b9c1-7d33-0410-9eda-942365e851bb |
61091743da1a9ed6dfd5e077fdcc972553358962 |
|
04-Apr-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
generalized Named to SenAttr to be useable by Logic.Prover as well
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7784 cec4b9c1-7d33-0410-9eda-942365e851bb |
7ba9ed9adedfae74bad2d3f8a26ffe6c83626446 |
|
23-Mar-2007 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
some documentation
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7750 cec4b9c1-7d33-0410-9eda-942365e851bb |
2a8ad76d9595e7e0d4d7d66ee4a4a62df6c9fb6b |
|
19-Mar-2007 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
moved datatype ProofGUIActions from GUI.ProofManagementTypes to Proofs/GUIState
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7707 cec4b9c1-7d33-0410-9eda-942365e851bb |
d4cb5f03c55f0aeff72f06dac61e1af24479ddd9 |
|
19-Mar-2007 |
Rainer Grabbe <rainer@informatik.uni-bremen.de> |
* recalculation of sublogic and KnownProversMap upon (de)selection of goals, axioms and proven theorems
* recalculation of list of comorphisms for "More fine grained selection...".
* additional button for showing selected theory
* all goals are selected from start of prove window
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7698 cec4b9c1-7d33-0410-9eda-942365e851bb |
171a9ed14ebfd5d90fe73edf33b72d793d01d75e |
|
19-Mar-2007 |
Razvan Pascanu <r.pascanu@jacobs-university.de> |
small changes
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7696 cec4b9c1-7d33-0410-9eda-942365e851bb |
c1f29a0f0c0b83858e7e57668dac254504f213b6 |
|
09-Mar-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
added old node label to SetNodeLab for undoing changes
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7631 cec4b9c1-7d33-0410-9eda-942365e851bb |
a4b3955462c5ba765a97f11af8b895aab145dd0d |
|
04-Mar-2007 |
Cui Jian <ken@informatik.uni-bremen.de> |
see ticket 268
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7597 cec4b9c1-7d33-0410-9eda-942365e851bb |
0f2be8b95750f4ac578e8a92ac6ef73b48526580 |
|
22-Feb-2007 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
moved things from todo lists into Trac
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7514 cec4b9c1-7d33-0410-9eda-942365e851bb |
ad270004874ce1d0697fb30d7309f180553bb315 |
|
21-Feb-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
switched to Data.Set, Data.Map and Data.Dynamic
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7491 cec4b9c1-7d33-0410-9eda-942365e851bb |
f4ae50539e67874b6162f8334f6782a0d66acefa |
|
21-Feb-2007 |
Cui Jian <ken@informatik.uni-bremen.de> |
see ticket 113
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7483 cec4b9c1-7d33-0410-9eda-942365e851bb |
33c33fde308de14d34177617a28524312f5f0ad8 |
|
16-Feb-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
replaced map_theory by wrapMapTheory for sublogic tests
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7457 cec4b9c1-7d33-0410-9eda-942365e851bb |
6a9b85953df4e29a996536ffc7dbf7ef9dbc64c7 |
|
28-Jan-2007 |
Cui Jian <ken@informatik.uni-bremen.de> |
changes from Ken, details see the cloesed tickets from Ken
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7352 cec4b9c1-7d33-0410-9eda-942365e851bb |
e6d40133bc9f858308654afb1262b8b483ec5922 |
|
01-Jan-2007 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
added Description header
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7287 cec4b9c1-7d33-0410-9eda-942365e851bb |
49588f3d624e56594d888bc622bc90618ae3c2c5 |
|
01-Jan-2007 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
added Description header
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7286 cec4b9c1-7d33-0410-9eda-942365e851bb |
a9ec05a03aaea02a63e2a9b5f60b823e54151f40 |
|
29-Dec-2006 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
description
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7283 cec4b9c1-7d33-0410-9eda-942365e851bb |
0ee3933098d65199ae39ea41cfc62634226dad15 |
|
20-Dec-2006 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
GUI/ConvertDevToAbstractGraph.hs:
* changed selector name
Proofs/InferBasic.hs GUI/ProofManagement.hs
GUI/ConvertDevToAbstractGraph.hs:
* added MVar which allows only one ProofManagement window at the same time.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7280 cec4b9c1-7d33-0410-9eda-942365e851bb |
e24d81c69aecd41abb2f4969519c9e7126b1d687 |
|
15-Dec-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
added indices to G_sign, GMorphism, G_morphism und G_theory
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7264 cec4b9c1-7d33-0410-9eda-942365e851bb |
f64f3dc78de82101483fe97bf109a42ca4d59d77 |
|
29-Aug-2006 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
preparations for the CMDLine proving interface
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6901 cec4b9c1-7d33-0410-9eda-942365e851bb |
6528ec34ad606aecb68cbeccd7408ea2a1e99a65 |
|
06-Jul-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
the class name must be exported for haddock
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6628 cec4b9c1-7d33-0410-9eda-942365e851bb |
ef7d1a1d5454458d46b9acefeda94b12bdc695b2 |
|
06-Jul-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed old PrettyPrint instances
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6609 cec4b9c1-7d33-0410-9eda-942365e851bb |
e550da81778d64d06c7950b1d578a1cc307ee280 |
|
23-May-2006 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
corrected proving via KnownProversMap
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6378 cec4b9c1-7d33-0410-9eda-942365e851bb |
2de8dfc30c926ee27254bfa32230a01435530efe |
|
17-May-2006 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
faster generation of all Provers/Comorphism pairs; each comorphism to prover/cons_checker is displayed with target tool
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6348 cec4b9c1-7d33-0410-9eda-942365e851bb |
724be620c516160e7d2c203999f01df4ccc53048 |
|
31-Jan-2006 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
Refactored Logic.Prover.Proof_status:
now a Record datatype with only two variants:
(1) Proof_status for goals
(2) Consistency
The status of a goal is now represented by a separate enumerated datatype:
GoalStatus
added field goalIsUsedInProof which should be True if the goal was in the
list of used formulae
other changes:
* improved display of proof details in GUI.ProofManagement
* added todo point for Isabelle.IsaProve
* Logic.Logic.Sentences demands Ord instancew for proof_tree now
so it was easier to derive the Ord instance of Proof_status automatically
* SPASS removes now the goal from the list of used axioms and stores the
derived information properly
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5750 cec4b9c1-7d33-0410-9eda-942365e851bb |
7f7460e7095628f3437b116ee78d3043d11f8feb |
|
18-Jan-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
generalized IOResult to ResultT
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5665 cec4b9c1-7d33-0410-9eda-942365e851bb |
04d04d19fdd5320953c78ad5b6d2d11f85bc4bcf |
|
17-Jan-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed type synonyms ProofStatus and LibNode
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5654 cec4b9c1-7d33-0410-9eda-942365e851bb |
333780eae2be9f20fe46dedbf5eb46ffa0cbfd02 |
|
13-Jan-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
incorporated ProofHistory into LibEnv as ProofStatus
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5637 cec4b9c1-7d33-0410-9eda-942365e851bb |
57d320fc4d0fe1a1c08cfe6cd9ebec09b86c2cbf |
|
09-Jan-2006 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
refactoring fixing the problem of circular dg proofs.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5618 cec4b9c1-7d33-0410-9eda-942365e851bb |
2272b992302eb61b2a039033cb8cdaf7809fe682 |
|
30-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed unused imports
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5578 cec4b9c1-7d33-0410-9eda-942365e851bb |
0206ab93ef846e4e0885996d052b9b73b9dc66b0 |
|
28-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
split off Automatic from InferBasic and checked with ghc-6.2.2
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5563 cec4b9c1-7d33-0410-9eda-942365e851bb |
eac3174ea16c143bfaeb3f2e2103a11a2f162c6c |
|
05-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
cleaned up a bit
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5491 cec4b9c1-7d33-0410-9eda-942365e851bb |
833baa690207430f9cc3ca599039954a7840fa30 |
|
29-Nov-2005 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
a disproved status is now only kept if all axioms were selected otherwise its dropped.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5466 cec4b9c1-7d33-0410-9eda-942365e851bb |
5ef395ccb7c654b00f393715176a0c8f9ae69b77 |
|
18-Nov-2005 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
* Implemented that the selection of sentences in the theory in the GUIState
is used in a proof.
* markProved now also considers Disproved and Open Proof_status'
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5435 cec4b9c1-7d33-0410-9eda-942365e851bb |
d19b839f3726cc508e3c52a7af227167a9e38f45 |
|
28-Oct-2005 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
GUIState:
* changed portable entry
InferBasic:
* DevGraph node gets result of prover now
* Edges have no information on proofs
ProofManagementGUI:
* goals are returned now
* status display is working
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5311 cec4b9c1-7d33-0410-9eda-942365e851bb |
5fcb1cb8c190e9bfb8d5c06c2e7d7a4b65f361ac |
|
28-Oct-2005 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
GUI
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5309 cec4b9c1-7d33-0410-9eda-942365e851bb |
9603ad7198b72e812688ad7970e4eac4b553837a |
|
25-Oct-2005 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
Refactoring of ThSens, Theory, SenStatus:
* SenStatus is now parametrised over a theoremStatus, too;
it is used for structured and basic theories;
value is no longer a (Named a);
isDef, isAxiom are now fields of SenStatus, too
* ThSens is not a Set any longer it is now a Common.OrderedMap.OMap
* Theory contains now a ThSens OMap with
theoremStatus == Proof_status proof_tree
version_nr is updated for changed ThSens structure
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5250 cec4b9c1-7d33-0410-9eda-942365e851bb |
54a0a1e10bd93721cf52dbd9b816c8f108997ec0 |
|
21-Oct-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
purified automatic and cleaned up a bit
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5219 cec4b9c1-7d33-0410-9eda-942365e851bb |
48c5e3928b13a41507bb892e745d3ede081b0b18 |
|
18-Oct-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
avoided IO monad for locDecomp
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5209 cec4b9c1-7d33-0410-9eda-942365e851bb |
ebdce567033765c1f16ccf25d721c02986a5da33 |
|
18-Oct-2005 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
Proved axioms were removed from the list of axioms which is sent to the Prover. No 2nd attempt to prove already proved goals.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5203 cec4b9c1-7d33-0410-9eda-942365e851bb |
b65e16b9e5652ff341ab0f49be5da51e2c0e10a5 |
|
18-Oct-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
introduced stabilities of logics
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5200 cec4b9c1-7d33-0410-9eda-942365e851bb |
062339789017952c527a799520dfe1b2e6b44368 |
|
18-Oct-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
fixed problem with wrong node number
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5199 cec4b9c1-7d33-0410-9eda-942365e851bb |
e509b6f97f98f96ef258c1c3f7968241da8bde5d |
|
18-Oct-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
fixed bug causing Match (graph) exception
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5198 cec4b9c1-7d33-0410-9eda-942365e851bb |
aebf36d7483e5c012eff154d0b76de400d8fe3fc |
|
13-Oct-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Refectoring: local proof goals also for DGRefs
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5176 cec4b9c1-7d33-0410-9eda-942365e851bb |
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0 |
|
29-Sep-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
expanded tabs to spaces
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5106 cec4b9c1-7d33-0410-9eda-942365e851bb |
42626cd6acc59504dff56b5b81043c272778c5fb |
|
23-Sep-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
refactored proof status info for sentences
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5063 cec4b9c1-7d33-0410-9eda-942365e851bb |
33fc94b09b906329ca7505caa1ddcddf67e3f8da |
|
17-Sep-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
enhanced basic inference: enter proof status returned from prover into DG node. Now nodes really can get green\!
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5021 cec4b9c1-7d33-0410-9eda-942365e851bb |
ef3c4d0483a81254f785bdbd3e5448fdabac7a84 |
|
16-Sep-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
renamed local subsumption into local inference
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5019 cec4b9c1-7d33-0410-9eda-942365e851bb |
709653bffee501341e2fdc55b9223e4921047c65 |
|
16-Sep-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
refactored basic inference and local subsume, according to theory in CASL RefMan, p. 308
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5018 cec4b9c1-7d33-0410-9eda-942365e851bb |
a059fb5629939bb0d74da56094b12bb793759f0c |
|
25-Aug-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
move Proofs.Proofs types to DevGraph
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4980 cec4b9c1-7d33-0410-9eda-942365e851bb |
5d812ccb300d5ca8b6e9474d2a644b964faf2d28 |
|
10-Aug-2005 |
Jorina Freya Gerken <jfgerken@gmx.de> |
added dgn_cons and dgn_cons_status to DGNode (in Static/DevGraph.hs)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4897 cec4b9c1-7d33-0410-9eda-942365e851bb |
7bf4436b6f9987b070033a323757b206c898c1be |
|
03-Aug-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
introduced type safe coercions, separated G_prover and G_cons_checker, partly removed G_ext_sign
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4854 cec4b9c1-7d33-0410-9eda-942365e851bb |
4ea99e115bbade1632815267d5e0dcb9931aac1e |
|
02-Aug-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
decorated theory sentences,renamed DevGraph.Open to LeftOpen,handcoded ATC/DevGraph.hs due to cyclic data types
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4843 cec4b9c1-7d33-0410-9eda-942365e851bb |
8a8880f1b6a0681e636480991d45dfea11d62ff8 |
|
29-Jul-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
used G_theory in DevGraph and removed G_l_sentences
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4829 cec4b9c1-7d33-0410-9eda-942365e851bb |
561943293cff00ce85a4baa0bb0b90d9d371f2b3 |
|
29-Jul-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
changed profile of computeTheory
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4824 cec4b9c1-7d33-0410-9eda-942365e851bb |
0cad947eaa4ce387599dbec645ad80fd2d87c53b |
|
27-Jul-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
corrected treatment of local theorems
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4805 cec4b9c1-7d33-0410-9eda-942365e851bb |
7e0f9d3c55f770f7a2a7b27babd06deda1c59b71 |
|
26-Jul-2005 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
* changed style of goal and theory translation for proving:
signature, axioms and goals are translated together with map_theory
now. This enables correct usage of Comorphisms which cannot translate
signature and sentences seperately.
* corrected an error message
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4780 cec4b9c1-7d33-0410-9eda-942365e851bb |
cd25621939b8f27c6c7e2933ece72bc2d91b00f7 |
|
15-Jul-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
corrected call of computeLocalTheory
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4681 cec4b9c1-7d33-0410-9eda-942365e851bb |
47e336bc89d1bd1038d7e3560291d0c085a86d9c |
|
15-Jul-2005 |
Jorina Freya Gerken <jfgerken@gmx.de> |
computeTheory now considers referenced libraries, too (snd try)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4674 cec4b9c1-7d33-0410-9eda-942365e851bb |
42c01284bba8d7c8d995c8dfb96ace57d28ed1bc |
|
15-Jul-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
refactoring: [Pos] replaced with Range in order to exclude positions from equality of abstract syntax
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4671 cec4b9c1-7d33-0410-9eda-942365e851bb |
08511aafa5540e9260248d52a3f9f0e453c29dfc |
|
30-Jun-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
corrected 'pover', deleted unused code (get it from previous revision if you need it)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4541 cec4b9c1-7d33-0410-9eda-942365e851bb |
3c4ad771f59dc788feb23665ce439734f8141f4b |
|
30-Jun-2005 |
Jorina Freya Gerken <jfgerken@gmx.de> |
__* empty log message __*
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4538 cec4b9c1-7d33-0410-9eda-942365e851bb |
c6d1878f9318c23e1a9e8540f5e83cfa8cbe1728 |
|
29-Jun-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
hack for avoiding problem with basic inference (no goals appear)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4528 cec4b9c1-7d33-0410-9eda-942365e851bb |
f3a94a197960e548ecd6520bb768cb0d547457bb |
|
15-Jun-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
aligned module description for haddock-0.7
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4438 cec4b9c1-7d33-0410-9eda-942365e851bb |
97018cf5fa25b494adffd7e9b4e87320dae6bf47 |
|
15-Jun-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
replaced Licence with License for haddock-07
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4433 cec4b9c1-7d33-0410-9eda-942365e851bb |
e220b2051a2342a9291721e6c7f408860bed01b7 |
|
14-Jun-2005 |
Jorina Freya Gerken <jfgerken@gmx.de> |
extended data ThmLinkStatus in Static/DevGraph.hs so that Proven now has also a DGRule
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4421 cec4b9c1-7d33-0410-9eda-942365e851bb |
12848428a357b0b096c3b88bd86b396c7f0e9116 |
|
08-Jun-2005 |
Jorina Freya Gerken <jfgerken@gmx.de> |
getAllLocGlobDefPathsTo in DGToSpec now searches in referenced libraries, too
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4391 cec4b9c1-7d33-0410-9eda-942365e851bb |
b9f1c1e07f18bf75aadcbba375e7558dc295df4e |
|
07-Jun-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed reexport of showPretty in Result
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4387 cec4b9c1-7d33-0410-9eda-942365e851bb |
120eec9ff1748e1ae786e2ab073234198bc0f701 |
|
01-Jun-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
splitted large Proofs file
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4355 cec4b9c1-7d33-0410-9eda-942365e851bb |
e5b79e9fe9606fd386dc840ea9f1514e7b9b32b9 |
|
01-Jun-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
added poor gui via console if uni is missing
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4353 cec4b9c1-7d33-0410-9eda-942365e851bb |
4e2331b387b90a234dc36b12c778914d3e202718 |
|
01-Jun-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
splitted off Proofs data types
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4352 cec4b9c1-7d33-0410-9eda-942365e851bb |