ML Anthology

A Definition-Driven Theorem Prover

George W. Ernst
IJCAI 1973 pp. 51-55
doi:10.1109/TC.1976.1674611 /ijcai/1973/ernst1973ijcai-definition/

Abstract

This paper describes a theorem prover, running on a PDP-10-Tenex system, that can prove some theorems whose statements involve a relatively large number of definitions. Such theorems require special methods because 1) their statements contain a large number of clauses and 2) their proofs are quite long although straightforward.

PDF Semantic Scholar

Cite

Text

Ernst. "A Definition-Driven Theorem Prover." International Joint Conference on Artificial Intelligence, 1973. doi:10.1109/TC.1976.1674611

Markdown

[Ernst. "A Definition-Driven Theorem Prover." International Joint Conference on Artificial Intelligence, 1973.](https://mlanthology.org/ijcai/1973/ernst1973ijcai-definition/) doi:10.1109/TC.1976.1674611

BibTeX

@inproceedings{ernst1973ijcai-definition,
  title     = {{A Definition-Driven Theorem Prover}},
  author    = {Ernst, George W.},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {1973},
  pages     = {51-55},
  doi       = {10.1109/TC.1976.1674611},
  url       = {https://mlanthology.org/ijcai/1973/ernst1973ijcai-definition/}
}