setup Isabelle's classical reasoner

spechub / Hets

The Heterogeneous Tool Set

http://hets.eu

GNU General Public License v2.0

57 stars 19 forks source link

setup Isabelle's classical reasoner #164

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/164

For each generated Isabelle theory, some of the axioms should be inserted as rules of appropriate type in the classical reasoner. See the Isabelle reference manual.

sternk commented 10 years ago

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

I leave this as a thesis for someone else to find "appropriate rules"