## Automated Theorem-proving in Non-classical Logics |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

NonClassical Logic and Automated TheoremProving | 1 |

TheoremProving for the Relevant Logic LR | 19 |

Algebraic Models | 71 |

Copyright | |

4 other sections not shown

### Other editions - View all

### Common terms and phrases

algebraic Algorithm Alternative pc Anderson and Belnap applied assessments ATP systems automated theorem-proving axioms Belnap 75 Bibel Chapter checks classical logic closed subtree Computer Science connective rules contraction database decision problem decision procedure deductive defined Definition derived axioms disjunction Dunn example finite formulation of LR Gentzen formulation Gentzen-style given global properties Idempotent Idempotent reducts inductive hypothesis intuitionistic logic invertible formulas KRIPKE Kripke's L3-provable L5-proof Lemma material implication matrix property McRobbie Meyer modal logic models Morgan monoids multiset multiset containing multiset ft n-ary function n-variable formulas negated Nilsson 80 node_state node-pruning non-classical logics non-monotonic Non-Monotonic Logic normal-forms obstinate nodes parametric positive/negative parts property premiss-sets premisses principal constituent problem proof procedures proof search tree proof-attempt proof-theoretic proper subalgebra propositional logic propositional variables prove pruned pst(a recursive passes refuting relevant ATP relevant logics Routley semantics Strategy subformulas Table techniques theorem theory unprovable Wrightson