×

zbMATH — the first resource for mathematics

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

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