Finding missing proofs with automated reasoning (Q5951893)
From MaRDI portal
scientific article; zbMATH DE number 1687393
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Finding missing proofs with automated reasoning |
scientific article; zbMATH DE number 1687393 |
Statements
Finding missing proofs with automated reasoning (English)
0 references
13 November 2002
0 references
The paper focuses on finding axiomatic proofs by using the automated reasoning program OTTER. Many of the proofs the authors have found are missing in the literature on logic. An example of such a missing proof concerns the Łukasiewicz 23-letter single axiom for two-valued calculus. Many of the proofs answer questions that remained open for decades.
0 references
condensed detachment
0 references
logic calculi
0 references
axiomatic proofs
0 references
automated reasoning program OTTER
0 references
