Consistency Checker GUI

[maeder]

GUI tasks:

• global menu
• offers batch mode to run consistency checks on all specs with darwin
• DevGraphGUI: implement color change/add additional symbol of/for inconsistent and consistent nodes

Followup tasks

• encapsulation of Isabelle refute
• displays a list of all specs/nodes (named and unnamed) with selection choices
• connection to different dedicated consistency checkers
• also provide an interface to conservativity checking oder the empty theory (this also entails consistency)

A rough idea for the look of the consistency checker guy is available via the attachment.

[luettich]

a prelimnary document describing some details about the needed implementations is checked into our CVS system at 'HetCATS/doc/ConsistencyCheckingGUI.tex' (the file compiles fine with pdflatex)

[luecke]

Idea for Consistency Checker Guy

[till]

Comment to the picture: Model finding, not model checking.

Why just CASL and TPTP as output languages? I think the output logic should be that of the input specification, and then, the model should be translatable against comorphisms. Of course, also "borrowing" of model finders should be possible. That is, the input specification is first translated along a comorphism into a model-finder-supported logic, a model is searched, and then the model is translated back against the comorphism (therefore, comorphisms should have a method for translating models).

[luecke]

A better interface idea

[maeder]

try to reuse as much from the prover GUI, i.e. port prover GUI to GTK later on

[maeder]

remove temporarily this unimplemented node menu for milestone 0.93

[maeder]

Apart from a global menu a local node menu would be better than just a list of comorphisms to select from.

[maeder]

the computed theories must be checked and should be cached together with their sublogics

[raider]

Implemented. Stop button works fine since changeset:12754