search

spechub / Hets

The Heterogeneous Tool Set
http://hets.eu
GNU General Public License v2.0
57 stars 19 forks source link

check dol files in COLORE with Hets, and try automatic proofs #1066

Open sternk opened 10 years ago

sternk commented 10 years ago

Reported by till and assigned to maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/1066

disprove_leu.log patch.diff periods.hpf owltime_leu.hpf disprove_le.log owltime_le.hpf libs

Try with "Edit -> Proofs -> Auto-DG-Prover" and then "Edit -> Automatic Proofs"

sternk commented 10 years ago

Comment by sschulze Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/1066#comment:1

Parsing fails:

$ hets -v2 -g ./complex/periods/mappings/periods.dol
Reading file ./complex/periods/mappings/periods.dol
### file name './complex/periods/mappings/periods.dol' does not match library name 'complex/periods/mappings/periodsdol'
Analyzing file ./complex/periods/mappings/periods.dol as library complex/periods/mappings/periodsdol
logic CommonLogic
Analyzing view http://code.google.com/p/colore/source/browse/trunk/ontologies/periods/periods.dol#i0
*** Error /home/soeren/hets/Hets-lib/CommonLogic/colore/./complex/periods/mappings/periods.dol:9.21-9.41,
structured specification 'http://code.google.com/p/colore/source/browse/trunk/ontologies/periods/periods_root' or 'Periods:periods_root' not found
hets: user error (Stopped due to errors)

What exactly is going on here? (OK, the given Periods: prefix is wrong, but changing it to the correct <http://code.google.com/p/colore/source/browse/trunk/ontologies/complex/periods/> doesn't fix anything.)

sternk commented 10 years ago

Comment by sschulze Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/1066#comment:2

After removing some views that led to errors (see the patch above), the SPASS prover (with the CommonLogic2CASLCompact comorphism) gave the following result:

periods:
[1/3] i1__T
[t] "periods"
[+] "periods_root"
[t] "periods_def"

[1/3] i2__T
[t] "approximate_point"
[t] "ap_def"
[+] "ap_root"

owltime_le: 
[2/3] i3__T
[t] "linear_ordering"
[+] "partial_ordering"
[+] "quasiorder"

[1/1] owltime_le
[+] "owltime_instant_s"

owltime_leu:
[2/3] i2__T
[t] "linear_ordering"
[+] "partial_ordering"
[+] "quasiorder"

For owltime_mleu.het, there was nothing to prove. Command to invoke Hets: .../colore/complex$ hets -Lcat libs-g periods/mappings/periods.het -g (resp. the other files) libs is the file above.

sternk commented 10 years ago

Comment by sschulze Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/1066#comment:3

In fact, linear_ordering can be disproved in both owltime_le and owltime_leu. For details, see the attachments.

sternk commented 10 years ago

Comment by sschulze Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/1066#comment:4

As of spechub/Hets@c8860ed27f3aeb6725fb47da42916b9555653ed1, Hets now automatically imports unknown IRIs in interpretations. This can also be done manually by the command "use", which has been implemented for debugging purposes. When foo:bar is an IRI, use foo:bar imports the specification bar from foo:bar. use foo:bar#baz imports baz from foo:bar.

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/1066#comment:8

Replying to sschulze:

As of [17617], Hets now automatically imports unknown IRIs in interpretations.

This has been changed, see #1235.

sternk commented 10 years ago

Comment by till Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/1066#comment:9

see http://www.ontohub.org/repositories/colore/errors for a quick overview of the errors.

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/1066#comment:10

Replying to till:

see http://www.ontohub.org/repositories/colore/errors for a quick overview of the errors.

I cannot reproduce these (1187?) errors. The .clif files of https://colore.googlecode.com/svn/trunk/ontologies mostly contain http cl-imports and the revision 1306 was last modified 2013-12-18. The few error messages that I looked at mostly showed relative path to files that could not be found or contained parse errors. My own first test showed an error in http://colore.googlecode.com/svn/trunk/ontologies/planar_mereology/atomic_transitive_tripartite.clif

maeder@turing:~/Hets-lib> find CommonLogic/colore -name \*.clif | xargs hets -C http://colore.oor.net=http://colore.googlecode.com/svn/trunk/ontologies -v2
Reading file CommonLogic/colore/planar_mereology/atomic_plane_mutual_dependence.clif
Reading CLIF file CommonLogic/colore/planar_mereology/atomic_plane_mutual_dependence.clif
Downloaded http://colore.googlecode.com/svn/trunk/ontologies/planar_mereology/atomic_plane_dependence.clif
Downloaded http://colore.googlecode.com/svn/trunk/ontologies/bipartite_incidence/partial_bipartite.clif
Downloaded http://colore.googlecode.com/svn/trunk/ontologies/bipartite_incidence/weak_bipartite.clif
Downloaded http://colore.googlecode.com/svn/trunk/ontologies/planar_mereology/atomic_transitive_tripartite.clif
hets: "http://colore.oor.net/planar_mereology/atomic_transitive_tripartite" (line 2, column 82):
unexpected ")"
expecting cl letter, "(" or sentence

The closing ")" is indeed wrong (the matching one is at the end of the file) but I cannot commit changes to this repository. Furthermore, the imports in http://colore.googlecode.com/svn/trunk/ontologies/planar_mereology/atomic_transitive_tripartite.clif do not exist.