| | | Bachmair, Leo
Ganzinger, Harald | | Resolution Theorem Proving
In: Handbook of Automated Reasoning, 19-99 | |
| | | Bockmayr, Alexander
Weispfenning, V. | | Solving numerical constraints
In: Handbook of Automated Reasoning, 751-842 | |
| | | Fermüller, Christian G.
Leitsch, Alexander
Hustadt, Ullrich
Tammet, Tanel | | Resolution Decision Procedures
In: Handbook of Automated Reasoning, 1793-1849 | |
| | | Ganzinger, Harald
Hustadt, Ullrich
Meyer, Christoph
Schmidt, Renate A. | | A Resolution-Based Decision Procedure for Extensions of K4
In: Advances in Modal Logic, Volume 2, 225-246 | |
| | | Nonnengart, Andreas
Ohlbach, Hans Jürgen
Gabbay, Dov M. | | Encoding two-valued non-classical logics in classic logic
In: Handbook of Automated Reasoning, 1403-1486 | |
| | | Nonnengart, Andreas
Weidenbach, Christoph | | Computing small clause normal forms
In: Handbook of Automated Reasoning, 335-367 | |