What people are saying - Write a review
We haven't found any reviews in the usual places.
Other editions - View all
A Resolution Principle for a Logic with Restricted Quantifiers
Limited preview - 1991
A-formulae Artificial Intelligence assignment automated theorem proving axiomatization background theory Biirckert classical resolution codomain concept descriptions conjunction constrained clauses constrained resolution constraint theories corresponding definite clause theory denoted derivable disequations disjunction disunification problem E-equality E-instance E-solution E-unification empty clause empty RQ-clause equational problems equational theory equivalent example existential closures existentially quantified feature logics feature symbols feature terms free algebra free constants free variables function symbols given Hence Herbrand universe idempotent initial algebra instance instantiation interpreted least Herbrand model Lemma literals negation notion order theory predicate logic predicate symbols query Resolution Principle restricted quantifiers restriction theory RQ-formulae RQ-resolution RQ-structure Schmidt-SchauB semantics semi-decidable set of variables Siekmann signature simple restrictions simplification system Skolem Skolem functions solutions solving sort restrictions sort structure sort symbols sort theory sort unification sorted logics subset substitutions with exceptions theorem proving undecidable unification problems unifiers universal quantifiers unsatisfiable VCoda well-sorted