General item icon

General item

A Framework of Refutational Theorem Proving for Saturation−Based Decision Procedures

Abstract:

Automated state-of-the-art theorem provers are typically optimised for particular strategies, and there are only limited number of options that can be set by the user. Probably because of this, the general conditions on applicability of saturation-based calculi have not been thoroughly investigated. However for some applications, e.g., for saturation-based decision procedures, one would like to have more options in order to design flexible saturation strategies. In this report we revisit seve...

Expand abstract

Actions


Authors


Yevgeny Kazakov More by this author
Publisher:
Max−Planck−Institut für Informatik
Publication date:
2005-08-01
URN:
uuid:26d0d55c-a9f5-4e8e-93a8-c010ed56a184
Local pid:
cs:877

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP