Logic Programming and Automated Reasoning: ... International Conference, LPAR ... : ProceedingsSpringer-Verlag, 1994 - Automatic theorem proving |
Contents
Generalization and Reuse of Tactic Proofs | 1 |
Program Tactics and Logic Tactics | 16 |
On the Relation Between the AuCalculus and the Syntactic Theory | 31 |
Copyright | |
19 other sections not shown
Other editions - View all
Common terms and phrases
A-calculus a₁ abstract abstract interpretation algorithm anti-link antiprenexing applied atom axiom bottom-up C₁ C₂ calculus called CBWK closed world assumption Computer Science conjunction constraint logic programming construct critical pair d-paths D₁ deduction defined definition denote derivation diagnoser disj disjunctive logic program equations event calculus example extended extraction finite domain first-order fixpoint formula framework function symbols goal independent analysis graph Harrop formulae Herbrand higher-order Higher-order abstract syntax higher-order logic implementation inconsistency induction hypothesis inference instantiated interpretation Kb₁ KbUS Lemma literal logic pro Logic Tactics multi-SLD multiset negation node operator predicate problem procedure Program Tactics programming language Prolog pruning quasi-reductive query rewrite rigid E-unification rule sequent Skolem terms SLD resolution solver st(P step substitution support-for-negation sets syntax t₁ techniques theorem proving tion top-down transformation unification uniform proof variables well-founded semantics