Automated theorem-proving in non-classical logics. (English) Zbl 0682.68097

Research Notes in Theoretical Computer Science. London: Pitman Publishing. 154 p. £15.95 (1988).
The topic of this book lies in the intersection of logic and computer science. It deals with automated theorem proving where the principal concern is with the design and implementation of theorem-proving programs for a range of non-classical logics. Especially, relevant logic is considered, culminating in the program KRIPKE for deciding theoremhood in the relevant logic LR. The proof-theoretic foundations of LR are also studied.
Reviewer: U.Schöning


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03F99 Proof theory and constructive mathematics