restricted-constraint-sentence is a predicate used to specify a class of sentences that are restricted by the set of operators and terminals in the grammar.The first argument is a KIF sentence, which must contain no quantification (i.e., no use of FORALL, EXISTS, SETOFALL, LAMBDA, or KAPPA).
The second argument is a class of logical operators (a class whose instances are a subset of {AND, OR, NOT, =>, <=, <=>}).
The third argument is a class of relation constants, such as '< and '=.
The fourth argument is a class of function constants, such as + and FIRST.
The fifth argument is a class of object constants allowed, which is some subset of OBJECT-CONSTANT. Instances of object-constant include symbols, numbers, and strings, but not lists or variables. One can use this argument to exclude some kinds of values by their syntatic form (e.g., strings) or limit the set of symbols to some pre-enumerated set.
One can use this predicate to specify sublanguages within KIF, such as constrain languages. One can denote classes of logical operators, relation constants, and function constants using the ONE-OF function and giving it quoted symbols as arguments. For example, the following specifies the class of sentences without negation or implication, whose only functions are the arithmetic operators, whose only relation is are equality, and whose object constants are symbols and numbers:
(restricted-constraint-sentence ?sentence
(one-of 'and 'or 'not)
(one-of '=)
(one-of '+ '- '* '/)
(kappa (?x) (and (object-constant ?x) (not (string ?x)))))
(Nth-Domain Restricted-Constraint-Sentence 1 Sentence)
(<=> (Restricted-Constraint-Sentence ?Sentence
?Class-Of-Logical-Operators
?Class-Of-Relation-Constants
?Class-Of-Term-Operators
?Class-Of-Object-Constants)
(And (Sentence ?Sentence)
(Not (Quantsent ?Sentence))
(Subclass-Of ?Class-Of-Logical-Operators Logical-Operator)
(Subclass-Of ?Class-Of-Relation-Constants
Relation-Constant)
(Subclass-Of ?Class-Of-Term-Operators Function-Constant)
(Subclass-Of ?Class-Of-Object-Constants Atomic-Term)
(Or (Exists
(?R @Tlist)
(And (= ?Sentence (Listof ?R @Tlist))
(Instance-Of ?R ?Class-Of-Relation-Constants)
(=> (Item ?T (Listof @Tlist))
(Restricted-Constraint-Term
?T
?Class-Of-Term-Operators
?Class-Of-Object-Constants))))
(Truth-Value-Constant ?Sentence)
(Exists
(?Op @Sentences)
(And (= ?Sentence (Listof ?Op @Sentences))
(Instance-Of ?Op ?Class-Of-Logical-Operators)
(=> (Item ?S (Listof @Sentences))
(Restricted-Constraint-Sentence
?S
?Class-Of-Logical-Operators
?Class-Of-Relation-Constants
?Class-Of-Term-Operators
?Class-Of-Object-Constants)))))))