Completion procedures as semidecision procedures
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN: 1611-3349, Vol: 516 LNCS, Page: 206-232
1991
- 5Citations
- 1Captures
Metric Options: CountsSelecting the 1-year or 3-year option will change the metrics count to percentiles, illustrating how an article or review compares to other articles or reviews within the selected time period in the same journal. Selecting the 1-year option compares the metrics against other articles/reviews that were also published in the same calendar year. Selecting the 3-year option compares the metrics against other articles/reviews that were also published in the same calendar year plus the two years prior.
Example: if you select the 1-year option for an article published in 2019 and a metric category shows 90%, that means that the article or review is performing better than 90% of the other articles/reviews published in that journal in 2019. If you select the 3-year option for the same article published in 2019 and the metric category shows 90%, that means that the article or review is performing better than 90% of the other articles/reviews published in that journal in 2019, 2018 and 2017.
Citation Benchmarking is provided by Scopus and SciVal and is different from the metrics context provided by PlumX Metrics.
Example: if you select the 1-year option for an article published in 2019 and a metric category shows 90%, that means that the article or review is performing better than 90% of the other articles/reviews published in that journal in 2019. If you select the 3-year option for the same article published in 2019 and the metric category shows 90%, that means that the article or review is performing better than 90% of the other articles/reviews published in that journal in 2019, 2018 and 2017.
Citation Benchmarking is provided by Scopus and SciVal and is different from the metrics context provided by PlumX Metrics.
Conference Paper Description
In this paper we give a new abstract framework for the study of Knuth-Bendix type completion procedures, which are regarded as semidecision procedures for theorem proving. First, we extend the classical proof orderings approach started in [6] in such a way that proofs of different theorems can also be compared. This is necessary for the application of proof orderings to theorem proving derivations. We use proof orderings to uniformly define all the fundamental concepts in terms of proof reduction. A completion procedure is given by a set of inference rules and a search plan. The inference rules determine what can be derived from given data. The search plan chooses at each step of the derivation which inference rule to apply to which data. Each inference step either reduces the proof of a theorem or deletes a redundant sentence. Our definition of redundancy is based on the assumed proof ordering. We have shown in [16] that our definition subsume those given in [50, 13]. We prove that if the inference rules are refutationally complete and the search plan is fair, a completion procedure is a semidecision procedure for theorem proving. The key part of this result is the notion of fairness. Our definition of fairness is the first definition of fairness for completion procedures which addresses the theorem proving problem. It is new in three ways: it is target oriented, that is it keeps the theorem to be proved into consideration, it is explicitly stated as a property of the search plan and it is defined in terms of proof reduction, so that expansion inferences and contraction inferences are treated uniformly. According to this definition of fairness, it is not necessary to consider all critical pairs in a derivation for the derivation to be fair. This is because not all critical pairs are necessary to prove a given theorem. Considering all critical pairs is an unnecessary source of inefficiency in a theorem proving derivation. We also show that the process of diproving inductive theorems by the so called inductionless induction method is a semidecision process. Finally, we present according to our framework, some equational completion procedures based on Unfailing Knuth-Bendix completion.
Bibliographic Details
http://www.scopus.com/inward/record.url?partnerID=HzOxMe3b&scp=0038687371&origin=inward; http://dx.doi.org/10.1007/3-540-54317-1_92; http://link.springer.com/10.1007/3-540-54317-1_92; http://link.springer.com/content/pdf/10.1007/3-540-54317-1_92.pdf; http://www.springerlink.com/index/10.1007/3-540-54317-1_92; http://www.springerlink.com/index/pdf/10.1007/3-540-54317-1_92; https://dx.doi.org/10.1007/3-540-54317-1_92; https://link.springer.com/chapter/10.1007/3-540-54317-1_92
Springer Science and Business Media LLC
Provide Feedback
Have ideas for a new metric? Would you like to see something else here?Let us know