| Author | Schellhorn, Gerhard | dc.contributor.author |
| Author | Reif, Wolfgang | dc.contributor.author |
| Date of accession | 2016-03-15T09:03:54Z | dc.date.accessioned |
| Available in OPARU since | 2016-03-15T09:03:54Z | dc.date.available |
| Year of creation | 1998 | dc.date.created |
| Abstract | The paper describes a large experiment in using automated theorem provers on first-order goals that showed up in a KIV case study on the verification of a Prolog compiler. Based on an algebraic specification with 456 axioms, 580 theorems were proven in KIV. For the theorems using induction, additional goals were generated for induction bases and steps, resulting in 733 noninductive goals. These were given to Otter, Setheo and Spass in several versions: with and without an axiom reduction preprocessing step, and with and without a precedence order generated from the specification structure. Test files are available in Otter syntax, as Setheo clauses and in the common syntax of the DFG-Schwerpunkt "Deduktion", which is used by Spass. | dc.description.abstract |
| Language | de | dc.language.iso |
| Publisher | Universität Ulm | dc.publisher |
| License | Standard | dc.rights |
| Link to license text | https://oparu.uni-ulm.de/xmlui/license_v3 | dc.rights.uri |
| Dewey Decimal Group | DDC 004 / Data processing & computer science | dc.subject.ddc |
| LCSH | Automatic theorem proving | dc.subject.lcsh |
| LCSH | Compilers (Computer programs) | dc.subject.lcsh |
| LCSH | Computer software; Verification | dc.subject.lcsh |
| Title | Theorems from compiler verification: a problem set for automated theorem provers | dc.title |
| Resource type | Bericht | dc.type |
| DOI | http://dx.doi.org/10.18725/OPARU-2501 | dc.identifier.doi |
| PPN | 1652464301 | dc.identifier.ppn |
| URN | http://nbn-resolving.de/urn:nbn:de:bsz:289-vts-85665 | dc.identifier.urn |
| GND | Automatisches Beweisverfahren | dc.subject.gnd |
| Faculty | Fakultät für Ingenieurwissenschaften und Informatik | uulm.affiliationGeneral |
| Date of activation | 2013-06-19T16:37:46Z | uulm.freischaltungVTS |
| Peer review | nein | uulm.peerReview |
| Shelfmark print version | QAA 5/A4.98,13 | uulm.shelfmark |
| DCMI Type | Text | uulm.typeDCMI |
| VTS ID | 8566 | uulm.vtsID |
| Category | Publikationen | uulm.category |
| uulm series | Ulmer Informatik-Berichte | uulm.seriesUlmName |
| Bibliography | uulm | uulm.bibliographie |
