What people are saying - Write a review
We haven't found any reviews in the usual places.
a mechanized logic for specification
A look at
10 other sections not shown
abstract data types algebra algorithm applied argument atomic atomic formulae automated theorem-proving program automatic axioms backtracking c-theory calculus clash-position closed world assumption COMPLEMENTARY complete condensed detachment conflict set constraints contains data structure data types database deduction defined delete demodulators denote derived elimination equations example exit finite formal formula function symbol given given-clause goal graph Homogenization Horn clauses implementation inference rules input integer Layer linear literal logic loop mathematics mating matrix reduction method minimal model natural deduction node non-monotonic non-monotonic logic object occurs pair paramodulant path position precondition predicate procedure proof proving query recursive representation language resolution result retcd com2 retrieval language semantic semantic network semigroup set of clauses solve specification subgoals substitution subtype term theorem prover theory Thue system Topologically sort type expression unifier variables