TERMINATOR

Antoniou, Grigoris; Ohlbach, Hans Jürgen

TERMINATOR

Download BibTeX Cite

Proceedings of the Eighth International Joint Conference on Artificial Intelligence. Theorem Proving. Pages 916-918.

Abstract

The Markgraf Karl Refutation Procedure (MKR-Procedure) is an automated theorem prover for sorted logic, based on an extended clause graph calculus, current-ly under development at the University of Karlsruhe . This paper describes th e TERMINATOR module, a component of the MKR-Procedure, which is essentially a very fast algorithm for the search for unit refutati o ns. The TERMINATOR is used as a fast pre-theorem prover as well as an integral component of the system , and is called for different tasks during the search for a proof.

Grigoris Antoniou, and Hans Jürgen Ohlbach. 1983. TERMINATOR. In Proceedings of the Eighth International Joint Conference on Artificial Intelligence, IJCAI-83. IJCAI, 916–918. https://ijcai.org/proceedings/1983/215

@inproceedings{ijcai1983p215,
  title     = {TERMINATOR},
  author    = {Antoniou, Grigoris and Ohlbach, Hans Jürgen},
  booktitle = {Proceedings of the Eighth International Joint Conference on
               Artificial Intelligence, {IJCAI-83}},
  publisher = {International Joint Conferences on Artificial Intelligence},
  editor    = {Alan Bundy},
  pages     = {916--918},
  year      = {1983},
  note      = {Theorem Proving},
  url       = {https://ijcai.org/proceedings/1983/215},
}

TY  - CPAPER
TI  - TERMINATOR
AU  - Antoniou, Grigoris
AU  - Ohlbach, Hans Jürgen
T2  - Proceedings of the Eighth International Joint Conference on Artificial Intelligence, IJCAI-83
PB  - International Joint Conferences on Artificial Intelligence
PY  - 1983
SP  - 916
EP  - 918
UR  - https://ijcai.org/proceedings/1983/215
ER  -