2001 | OriginalPaper | Buchkapitel
Adaptive Saturation-Based Reasoning
verfasst von : Alexandre Riazanov, Andrei Voronkov
Erschienen in: Perspectives of System Informatics
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
For most applications of first-order theorem provers a proof should be found within a fixed time limit. When the time limit is set, systems can perform much better by using algorithms other than the ordinary complete ones. In this paper we describe the Limited Resource Strategy intended to improve performance of resolution- and paramodulation- based provers when a fixed limit is imposed on the time of a run. We give experimental evidence that the Limited Resource Strategy gives a significant improvement over the OTTER saturation algorithm, algorithms not using passive clauses for simplification and the weightbased algorithms.