search

spechub / Hets

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

Write a parser for DFG-Syntax #370

Closed sternk closed 10 years ago

sternk commented 10 years ago

Reported by luecke and assigned to jiang Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/370

Design a Parser using the existing parsing infrastructure of Hets for the dfg-Syntax of the SPASS theorem prover. A link to the Syntax can be found at: http://spass.mpi-sb.mpg.de/download/binaries/spass-input-syntax15.pdf An existing Parser can be found at Hets/SPASS/DFGParser.hs, but note that this one is incomplete. You may use it as a source of inspiration, but a better implementation would be fine, and you should support all language features of DFG. And even the clause-formula-relation of SPASS 2.8+ is needed. The output of your parser is SPASS/SoftFOL abstract Syntax.

sternk commented 10 years ago

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

The Sign in SoftFOL is modified. clause-formula-relation, proof-list and setting-list are supported with respect to spass-input-syntax V1.5.