## Automated theorem proving |

### What people are saying - Write a review

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

### Contents

Logical rules | 6 |

The semantics of propositional logic | 21 |

Consistency completeness and confluence | 40 |

Copyright | |

35 other sections not shown

### Common terms and phrases

active path actually algorithm applied Automated Theorem Proving axioms called cg-resolution chapter clause complete connection calculus connection method connection proof consider contains convention deduction defined definition deleted denote discussed encoded eq-connection eq-literal existential quantifier extension F in normal F is complementary F is valid fact figure first-order level first-order logic formula F further goto ground level Hence Herbrand Herbrand's theorem higher-order logic Horn clauses illustrated implies induction labeled lemma logic program mathematical matrix F modus ponens natural deduction nodes Note obtained obviously occur paramodulation path through F predicate present proof system propositional logic Rc,t reader redundant relation representation represented resolution proof restricted result Sc,t selected set of connections Skolem functions Skolem normal form spanning set step STEP1 structure subformula subgoals substitution theorem proving tion top of WAIT tree trivial unification unifier valid formulas valid iff variable