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 |
42e78fd3454812d4f98b06154fdabc5ec3488718 |
|
29-Feb-2016 |
mcodescu <mscodescu@gmail.com> |
static analysis of intersections |
55ab20b85d8838544a83c1ef2e01e1f2b2da7496 |
|
04-Jan-2015 |
Eugen Kuksa <eugenk@informatik.uni-bremen.de> |
Add prover output to ProofStatus and xml response. |
0a65899b09e78455a94af9128455f6613441ab71 |
|
23-Oct-2014 |
cmaeder <cmaeder@users.noreply.github.com> |
added reasons for missing provers, etc |
e24ad3f655daa60ddabe690e4b11de3187996c16 |
|
22-Oct-2014 |
cmaeder <cmaeder@users.noreply.github.com> |
moved the IO availability test into the prover and checker records |
1a38107941725211e7c3f051f7a8f5e12199f03a |
|
08-Oct-2014 |
cmaeder <cmaeder@users.noreply.github.com> |
added a bunch of deriving Typeable and Data |
04857331be117d4e2215d866c309a17bd9a7e15c |
|
16-Aug-2013 |
Loredana Mihaela Diaconu <lo.diaconu@jacobs-university.de> |
disprove function
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@18130 cec4b9c1-7d33-0410-9eda-942365e851bb |
c3025f15666e968b6605b15d8d83cc1ee9f25169 |
|
03-May-2013 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
typo
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17938 cec4b9c1-7d33-0410-9eda-942365e851bb |
c042f761b11618eba28b1bbe67611ea1a2a1596f |
|
27-Feb-2013 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed unused code
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17769 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 |
f1af441c245fbecb3453fa730eed772519f293cc |
|
02-Jun-2010 |
Christian Maeder <Christian.Maeder@dfki.de> |
added LANGUAGE pragma
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13483 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 |
cf4e3ef8ae405824ae1bd39be9762e207836c0e0 |
|
26-Nov-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored ordered maps
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12858 cec4b9c1-7d33-0410-9eda-942365e851bb |
20d23303e7bef61d5d975d96a53bb9e971305297 |
|
26-Nov-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed unused map functions
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12855 cec4b9c1-7d33-0410-9eda-942365e851bb |
b6a79d36b19720a929a6d838889c374252ee2cd6 |
|
26-Nov-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
added type signature
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12854 cec4b9c1-7d33-0410-9eda-942365e851bb |
f30f834d81e1c294aff8eb2752fd864f6488820d |
|
26-Nov-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed unused genericCMDLautomatic
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12853 cec4b9c1-7d33-0410-9eda-942365e851bb |
c4f60523b8884f25d3d2c6950db6901425fb2fb6 |
|
20-Nov-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
revert changeset 12847 since provers are unable to proof all theorems identical to axioms
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12850 cec4b9c1-7d33-0410-9eda-942365e851bb |
74e513dd8ebc883d314d63ff3ca8eae52e5d0921 |
|
19-Nov-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
keep all theorems
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12847 cec4b9c1-7d33-0410-9eda-942365e851bb |
4b59523909ca1636387585da64baa491663634cb |
|
18-Nov-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
compute theories differently and start to set pending edges
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12842 cec4b9c1-7d33-0410-9eda-942365e851bb |
2f1781ab0a0a58328ef9d1ad8bda1984fd80259d |
|
10-Nov-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
only use two states proved consistent or inconsistent
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12816 cec4b9c1-7d33-0410-9eda-942365e851bb |
d1c15b86fa5f1b34ef777ff740a4bc9ae7fd0a54 |
|
03-Nov-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
refactored consistency checker interface
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12778 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 |
54ea981a0503c396c2923a1c06421c6235baf27f |
|
26-Sep-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
use a single Conservativity data type
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12527 cec4b9c1-7d33-0410-9eda-942365e851bb |
f3d52eea8d4138fd574e0fdecd6cf16dc9ea793c |
|
11-Sep-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
use automatic consistency checkers (automaticBatch is unused)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12458 cec4b9c1-7d33-0410-9eda-942365e851bb |
6f0be2db2f8bc6bd826fd41cd28cdf56d890cf49 |
|
03-Sep-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
add moved theorems to local inference rule
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@12408 cec4b9c1-7d33-0410-9eda-942365e851bb |
427aeade34f2771c0295250e9a94b89489bb9204 |
|
15-Jun-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
try to avoid too many overlapping sentence names
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11798 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 |
b3d0cacf580edf444a1fa2c1250923ea69714965 |
|
17-Feb-2009 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed unused CMDLinteractive
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11397 cec4b9c1-7d33-0410-9eda-942365e851bb |
386ffcce39ca7466c27a0a831fe4bbbbfd5c3632 |
|
28-Nov-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
added reasons to open proof states
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11120 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 |
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 |
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 |
cb8f1b02c57bc6bf2c904b561c1312a982ac85ab |
|
14-Nov-2008 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
flag for cofree links
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@11006 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 |
ce8e65eff6d8c22c974aeb31b5c954ff38105ebc |
|
08-Oct-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
changed mapThSensValue to monadic version mapThSensValueM
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10787 cec4b9c1-7d33-0410-9eda-942365e851bb |
816d8230f31347228e5cca026f73be49e3bfce53 |
|
06-Oct-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
avoid type sysnonym in instance head
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10772 cec4b9c1-7d33-0410-9eda-942365e851bb |
a129422b14eea673dc481d2553cec108e35e72ef |
|
06-Oct-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
added and used nameAndDisambiguate
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10770 cec4b9c1-7d33-0410-9eda-942365e851bb |
9159452d41e00128e4d0a6c252d8c84ecd95b988 |
|
25-Sep-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
marked non-portable
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10743 cec4b9c1-7d33-0410-9eda-942365e851bb |
0fd3d192643c2c048968879f39cb1f24b1e76ef2 |
|
25-Sep-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
added documentation
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10739 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 |
528f2d8f15b0cae81f02b34a74dbd744dffbba99 |
|
27-Aug-2008 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
corrected call of conservativity check: use whole theory of target node, not just local axioms
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10591 cec4b9c1-7d33-0410-9eda-942365e851bb |
3a6c7a7ff823616f56cd3d205fc44664a683effd |
|
01-Aug-2008 |
Christian Maeder <Christian.Maeder@dfki.de> |
shortened too long lines
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@10430 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 |
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4 |
|
17-Jan-2008 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
restored test function for CASL basic specs
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9446 cec4b9c1-7d33-0410-9eda-942365e851bb |
3052331838145bacc841740d8a123118e553cba5 |
|
25-Oct-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
added a field to Named for simplifier annotations #170
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9084 cec4b9c1-7d33-0410-9eda-942365e851bb |
e7b5c0df35a6c913170d892bb601298bc141b824 |
|
23-Oct-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
derived Typeable, cleaned up parser
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@9074 cec4b9c1-7d33-0410-9eda-942365e851bb |
135bcb7f65991146c103e5e7599adbc49fe7359d |
|
16-Aug-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
replaced senName with senAttr
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8627 cec4b9c1-7d33-0410-9eda-942365e851bb |
80d0480a60b409d9cf256d0a6c411dd99c672124 |
|
15-Aug-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
cleaned up Logic.Prover
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8621 cec4b9c1-7d33-0410-9eda-942365e851bb |
8b74f1cc678e4c018c79ec6d14c643389b429532 |
|
23-Jul-2007 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
added possibility to wait for each attempt of the batch mode for the CMDL interface; added test that can be run with "SoftFOL/tests/CMDL_tests batch"; updated documentation
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8451 cec4b9c1-7d33-0410-9eda-942365e851bb |
03f1cdf920c28b4d0f1ec047a4807851949d354e |
|
13-Jul-2007 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
* improved documentation of Logic.Prover
* added some threadDelay to BatchProcessing
* some modifications to the selection of all goals in PGIP
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8361 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 |
fe5c659e3a90e4622d0f189d6721e595533d2c85 |
|
31-May-2007 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
added timeUsed field to Logic.Prover.ProofStatus
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7956 cec4b9c1-7d33-0410-9eda-942365e851bb |
6970af7871bdbcfd1088d7d0658558ca312e771d |
|
10-May-2007 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
corrected comparison functions for joinSens and diffSens; they had been damaged by merging Named and SenStatus into SenAttr
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7886 cec4b9c1-7d33-0410-9eda-942365e851bb |
97e40034e4daabb29f0aba88a5809e50fc743861 |
|
09-May-2007 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
merged markAsAxiom and markAsFormerTheorem; former theorems keep their status over multiple imports
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7884 cec4b9c1-7d33-0410-9eda-942365e851bb |
1d5b2a1b3cba9e243b56abed8acdc5b9254b1a31 |
|
25-Apr-2007 |
Rainer Grabbe <rainer@informatik.uni-bremen.de> |
Axioms will not be declared as "former theorems" anymore.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7847 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 |
1686123f83910af58fba6c996bf7264702b3bc45 |
|
31-Mar-2007 |
Rainer Grabbe <rainer@informatik.uni-bremen.de> |
Imported theorems are marked with '(Th)' for proofs in ProofManagementGUI. Record types Logic.Prover.SenStatus and Common.AS_Annotation.Named were extended by field wasTheorem.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7765 cec4b9c1-7d33-0410-9eda-942365e851bb |
405a5a91feaf41b0f7c623521ac85e37109b60a5 |
|
01-Mar-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
avoided comparing from Common.Utils
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7577 cec4b9c1-7d33-0410-9eda-942365e851bb |
8c4df6ec540b2a1cfb897ed91ddbeea8b604bc54 |
|
23-Feb-2007 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
moved todo to trac
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7526 cec4b9c1-7d33-0410-9eda-942365e851bb |
705d04a6d3b01afd249f53397e5cbfa76fc0e179 |
|
21-Feb-2007 |
Christian Maeder <Christian.Maeder@dfki.de> |
replaced Data.Dynamic by Data.Typeable and removed trailing blanks
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7497 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 |
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 |
0095c7efbddd0ffeed6aaf8ec015346be161d819 |
|
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@7284 cec4b9c1-7d33-0410-9eda-942365e851bb |
4c917547d63648de43e36cb01e54953cb3915612 |
|
25-Nov-2006 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
Changed reference to result of Logic.Prover.proveCMDLautomaticBatch from
IORef to a thread-safe usage of MVar.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7203 cec4b9c1-7d33-0410-9eda-942365e851bb |
44551d3ad7d8ae6e282bc695c200609a9cb74603 |
|
06-Nov-2006 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
use error "msg" instead of undefined
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7125 cec4b9c1-7d33-0410-9eda-942365e851bb |
81bc059e878640f897258de3e319fe2025a5622c |
|
20-Oct-2006 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
introduced map functions for proof trees
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7080 cec4b9c1-7d33-0410-9eda-942365e851bb |
c8c4fdc0a61c88aac531495032b8610791526e9f |
|
19-Oct-2006 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
added comment for Rainer
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7067 cec4b9c1-7d33-0410-9eda-942365e851bb |
f43321aca70c37a1a6fe7d463f1525ae9ebf9413 |
|
05-Sep-2006 |
Rainer Grabbe <rainer@informatik.uni-bremen.de> |
Set Tactic_script back to String (in Logic.Prover), using ATPTactic_script for SoftFOL.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6920 cec4b9c1-7d33-0410-9eda-942365e851bb |
484cc3037eacfe410943446f7038b08c731c2115 |
|
01-Sep-2006 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
changed profile of proveCMDLautomaticBatch slightly
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6913 cec4b9c1-7d33-0410-9eda-942365e851bb |
a65b43ff55c1b66363eed3564f86266064fa449f |
|
30-Aug-2006 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
added automatic batch mode function
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6905 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 |
2870844cf0e81c9e2c24a7fa18cc2bdfe84d3a46 |
|
15-Aug-2006 |
Rainer Grabbe <rainer@informatik.uni-bremen.de> |
* changed Tacticscript type (see in Logic.Prover)
* improved output for MathServ-based provers, now displayed with Pretty
* improved display of box "save prover configuration" in GUI.GenericATP, using Pretty functions in module GUI.PrintUtils
* added field timeUsed in GenericConfig. It should contain number of milliseconds for a prover run. Already filled in SPASS and MathServ-based provers.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6820 cec4b9c1-7d33-0410-9eda-942365e851bb |
2c839e02e7c8732f1e4af2b2d87a2055de4a98c6 |
|
03-Jul-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
made Show a subclass of Pretty for debugging
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6567 cec4b9c1-7d33-0410-9eda-942365e851bb |
23a00c966f2aa8da525d7a7c51933c99964426c0 |
|
30-Jun-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
moved class Pretty from Doc to DocUtils
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6555 cec4b9c1-7d33-0410-9eda-942365e851bb |
e3c456d1e0b80a9d3d5d3edc3eb713da93967330 |
|
29-Jun-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed unused imports
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6538 cec4b9c1-7d33-0410-9eda-942365e851bb |
f354dda3b8e53f68805ea12ca89440908eae3029 |
|
23-Jun-2006 |
Christian Maeder <Christian.Maeder@dfki.de> |
removed PrettyPrint
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6497 cec4b9c1-7d33-0410-9eda-942365e851bb |
e42eddbc69dd31f7cd696e38f82acad678831cb7 |
|
31-May-2006 |
Jian Chun Wang <wjch868@informatik.uni-bremen.de> |
change to new Doc
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6408 cec4b9c1-7d33-0410-9eda-942365e851bb |
32a1e22f5776aa1132987c3abc2f3963da8d768c |
|
30-May-2006 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
Proved theorems with nothing known about consistency are displayed without (unknown) now
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6405 cec4b9c1-7d33-0410-9eda-942365e851bb |
2caa469afa557120b12fea247fd2078892ab52f9 |
|
19-Apr-2006 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
changed openProof_status
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6214 cec4b9c1-7d33-0410-9eda-942365e851bb |
f30a4b368eb2dca0d2da4415fef60dc226bc52d7 |
|
23-Mar-2006 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
typo
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6111 cec4b9c1-7d33-0410-9eda-942365e851bb |
5c7228df8b5c735df42d849ffde9cbb96958a849 |
|
23-Mar-2006 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
* removed field goalUsedInProof from Logic.Prover.SenStatus
* instead GoalStatus.Proved has a Parameter indicating the consistency
(similiar to the SZS Ontology)
* introduced a new StatusIndicator for Proved theorems in an inconsistent
theory
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@6109 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 |
8d97ef4f234681b11bb5924bd4d03adef858d2d2 |
|
30-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
derive Typeable along with ATC
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5572 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 |
e51568cd733ccb83a799f48f0802095e3f3a8d62 |
|
08-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
added markAsAxiom
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5504 cec4b9c1-7d33-0410-9eda-942365e851bb |
87ab788adadc73fd49e3c762caee6a88f844a5bc |
|
07-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
moved naming and disambiguation to toThSens and removed it from prepareSenNames
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5496 cec4b9c1-7d33-0410-9eda-942365e851bb |
c8502cadb0d13b572d270fe8218ca1397576a79b |
|
02-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
remove the overly redundant disambiguations (accidentally included)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5487 cec4b9c1-7d33-0410-9eda-942365e851bb |
c6c52abe702b71ddaae2b765c1e074d053adbe03 |
|
02-Dec-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
added diffSens and changed Ord SenStatus
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5485 cec4b9c1-7d33-0410-9eda-942365e851bb |
48fd7a27ee103bd46c8993836280985bddebb6b3 |
|
29-Nov-2005 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
corrected a bug that merged axioms with theorems if they were equal.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5465 cec4b9c1-7d33-0410-9eda-942365e851bb |
fdc1f76c4cf2698b07499034abd698f9fe4f56af |
|
18-Nov-2005 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
added record selector goalName for Open and Disproced in datatype Proof_status
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5431 cec4b9c1-7d33-0410-9eda-942365e851bb |
ef4b978a005bdccb8bd5e611887661db703114f2 |
|
27-Oct-2005 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
Added Ord instance for Proof_status
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5285 cec4b9c1-7d33-0410-9eda-942365e851bb |
7ac39d81b73fc2760422a1d0007cf694d0665c40 |
|
26-Oct-2005 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
joinSens integrates structural equal formulas into one formula, again
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5271 cec4b9c1-7d33-0410-9eda-942365e851bb |
311b77502c0485080ff5021cfd7f7d3c0ede68b5 |
|
25-Oct-2005 |
Klaus Luettich <luettich@informatik.uni-bremen.de> |
removed comment
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@5252 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 |
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 |
a7980a1cc2fa86d1b702ff530dc08d8a868928e2 |
|
01-Jul-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
added theorems and goals to used axioms
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4547 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 |
b4fbc96e05117839ca409f5f20f97b3ac872d1ed |
|
13-Jun-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
added maintainers
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4412 cec4b9c1-7d33-0410-9eda-942365e851bb |
0fddbb5238b6c7e7b7889597b5fa292f9bcbaf99 |
|
31-May-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
changed Proof_status that is still unused
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4346 cec4b9c1-7d33-0410-9eda-942365e851bb |
8b5f9f72ba210940b26034bcadd34b2fe7f93bbd |
|
31-May-2005 |
Christian Maeder <Christian.Maeder@dfki.de> |
restructered Logic.Prover
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4345 cec4b9c1-7d33-0410-9eda-942365e851bb |
b88799233dfad20f506173258cda9c48eae76a6e |
|
27-May-2005 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
commented tactic script
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4336 cec4b9c1-7d33-0410-9eda-942365e851bb |
5308ef83ee1b668f4cf6c8278bc645e7e0f8b4ed |
|
26-Nov-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Connected Isabelle consistency checker
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3468 cec4b9c1-7d33-0410-9eda-942365e851bb |
8ddc7a5666b6887cf3a2c7c29e4691e04373545f |
|
26-Nov-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Added consistency checking of nodes
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3466 cec4b9c1-7d33-0410-9eda-942365e851bb |
7ed2a775680fb1a29e6907d372124906b7746420 |
|
15-Nov-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Proof status interface reduced to names of axioms/thms
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3429 cec4b9c1-7d33-0410-9eda-942365e851bb |
9e2e744c6b967c3f5f581acf01c13769b6769285 |
|
02-Sep-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Added Eq and Show instances for DGRule. Needed refactoring of dynamics stuff
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3125 cec4b9c1-7d33-0410-9eda-942365e851bb |
59fa9b1349ae1e001d996da732c4ac805c2938e2 |
|
06-May-2004 |
Christian Maeder <Christian.Maeder@dfki.de> |
adaptions for ghc-6.3: mkAppTy -> mkTyConApp
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@2556 cec4b9c1-7d33-0410-9eda-942365e851bb |
aa0ef8adb2833838c1954e6f93c61d85d2cb226a |
|
14-Mar-2004 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Prover interface cont'd
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@2275 cec4b9c1-7d33-0410-9eda-942365e851bb |
306763c67bb99228487345b32ab8c5c6cd41f23c |
|
12-Feb-2004 |
Christian Maeder <Christian.Maeder@dfki.de> |
adapted headers
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@2158 cec4b9c1-7d33-0410-9eda-942365e851bb |
b09c4ce9ee62d8b62f6c7bb12956a3dea4defd95 |
|
25-Jul-2003 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
DG proofs added (initial version)
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@1599 cec4b9c1-7d33-0410-9eda-942365e851bb |
e3c9174a782e90f965a0b080c22861c3ef5af12d |
|
02-May-2003 |
Till Mossakowski <mossakow@iws.cs.uni-magdeburg.de> |
Added data construct to structured specs.
Adapted CspCASL parser to this.
New structure for hets.hs.
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@1305 cec4b9c1-7d33-0410-9eda-942365e851bb |
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bb |
|
24-Feb-2003 |
Christian Maeder <Christian.Maeder@dfki.de> |
introduced qualified names
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@972 cec4b9c1-7d33-0410-9eda-942365e851bb |
dbdae9a7cd57a9080536a5fce4ae52be5fe69081 |
|
21-Feb-2003 |
Christian Maeder <Christian.Maeder@dfki.de> |
moved to Logic sudirectory
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@943 cec4b9c1-7d33-0410-9eda-942365e851bb |