Please use this identifier to cite or link to this item:
doi:10.22028/D291-40193 | Title: | Using Theory Resolution to Simplify Interpreted Formulae |
| Author(s): | Socher-Ambrosius, Rolf |
| Language: | English |
| Year of Publication: | 1988 |
| Place of publication: | Kaiserslautern |
| DDC notations: | 004 Computer science, internet |
| Publikation type: | Report |
| Abstract: | Loveland & Shostak (1980) gave an algorithm for converting a decision procedure for ground formulae in a first-order theory to a simplifier for such formulae. The algorithm is supposed to produce a simplest clause set among all formulae built from atoms of the original formula. In this paper it is shown that this method does not meet this requirement. Furthermore we show that theory resolution can be used to extend Quine’s method to an algorithm that really accomplishes the task of simplifying interpreted formulae. |
| Link to this record: | urn:nbn:de:bsz:291--ds-401933 hdl:20.500.11880/37663 http://dx.doi.org/10.22028/D291-40193 |
| Series name: | SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447] |
| Series volume: | 88,16 |
| Date of registration: | 17-May-2024 |
| Faculty: | SE - Sonstige Einrichtungen |
| Department: | SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz |
| Professorship: | SE - Sonstige |
| Collections: | SciDok - Der Wissenschaftsserver der Universität des Saarlandes |
Files for this record:
| File | Description | Size | Format | |
|---|---|---|---|---|
| SEKI-Report-SR-88-16_Socher=Ambrosius_Using-Theory-Resolution-to-Simplify-Interpreted-Formulae.pdf | 1,01 MB | Adobe PDF | View/Open |
Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.