https://scholars.lib.ntu.edu.tw/handle/123456789/117200
DC 欄位 | 值 | 語言 |
---|---|---|
dc.contributor.author | Bonacina, M. P. | zh-TW |
dc.contributor.author | 項潔 | zh-TW |
dc.contributor.author | Hsiang, Jieh | en |
dc.creator | Bonacina, M. P.; Hsiang, Jieh | - |
dc.date | 1994 | en |
dc.date.accessioned | 2009-02-03T07:57:38Z | - |
dc.date.accessioned | 2018-07-05T01:30:30Z | - |
dc.date.available | 2009-02-03T07:57:38Z | - |
dc.date.available | 2018-07-05T01:30:30Z | - |
dc.date.issued | 1994 | - |
dc.identifier.uri | https://www.scopus.com/inward/record.uri?eid=2-s2.0-0038348878&doi=10.1016%2f0304-3975%2894%2900187-N&partnerID=40&md5=cf9e3a6ef9f500450cf5cc0ba0fc4ac7 | - |
dc.description.abstract | Completion procedures, originated from the seminal work of Knuth and Bendix, are well-known as procedures for generating confluent rewrite systems, i.e. decision procedures for equational theories. In this paper we present a new abstract framework for the utilization of completion procedures as semidecision procedures for theorem proving. The key idea in our approach in that a semidecision process should be target-oriented, i.e. keep into account the target theorem to be proved. For the inference rules of a completion procedure, we present target-oriented schemes of contraction inference rules, i.e. inference rules that delete sentences which are redundant for proving the target. For the search plan, we give a target-oriented, definition of fairness, according to which not all critical pairs need to be considered. We prove that our notion of fairness, together with the refutational completeness of the inference rules, is sufficient for a completion procedure to be a semidecision procedure. By relaxing the requirement of considering all critical pairs, our target-oriented framework should be more suitable for designing efficient procedures for theorem proving. The generation of decision procedures is included as a special side-effect and all the results of the classical approach to completion are re-obtained in our framework. The application of completion to disprove inductive conjectures, i.e. the so-called inductionless induction method, is also covered as a semidecision process. Finally, we present according to our framework, some equational completion procedures based on unfailing Knuth-Bendix completion. © 1995. | - |
dc.language | en | en |
dc.language.iso | en_US | - |
dc.relation | Theoretical Computer Science, 43, p. | en |
dc.relation.ispartof | Theoretical Computer Science | - |
dc.title | Towards a Foundation of Completion Procedures as Semidecision Procedures | - |
dc.type | journal article | en |
dc.identifier.doi | 10.1016/0304-3975(94)00187-N | - |
dc.identifier.scopus | 2-s2.0-0038348878 | - |
item.fulltext | with fulltext | - |
item.grantfulltext | open | - |
dc.relation.pages | 199-242 | - |
dc.relation.journalvolume | 146 | - |
dc.relation.journalissue | 1-2 | - |
dc.identifier.uri.fulltext | http://ntur.lib.ntu.edu.tw/bitstream/246246/118485/1/10.pdf | - |
item.openairecristype | http://purl.org/coar/resource_type/c_6501 | - |
item.openairetype | journal article | - |
item.languageiso639-1 | en_US | - |
item.grantfulltext | open | - |
item.cerifentitytype | Publications | - |
item.fulltext | with fulltext | - |
crisitem.author.dept | Networking and Multimedia | - |
crisitem.author.dept | Computer Science and Information Engineering | - |
crisitem.author.orcid | 0000-0002-2649-4331 | - |
crisitem.author.parentorg | College of Electrical Engineering and Computer Science | - |
crisitem.author.parentorg | College of Electrical Engineering and Computer Science | - |
顯示於: | 資訊工程學系 |
在 IR 系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。