Abstract:
Type quantifier language and calculus as logical positively-constructed means of knowledge representation and automation of deductive inference have been developed. In them, the type conditions of quantifiers can contain negations, and the calculus has completeness with respect to derivability in the classical predicate calculus.
Keywords:knowledge representation, logical inference, automatic proof of theorems.
