Class FUNCTION-CONSTANT

• Defined in theory: Parametric-constraints
• Source code: parametric-constraints.lisp

Slots on this class:

Documentation:

A function constant is a symbol that denotes a KIF function.

Instance-Of: Class

Alias: Funconst

Other Related Axioms:

(Restricted-Constraint-Sentence ?Sent
                                Logical-Operator
                                Relation-Constant
                                Function-Constant
                                Atomic-Term)

(=> (Constraint-Expression ?Sent)
    (Restricted-Constraint-Sentence ?Sent
                                    Logical-Operator
                                    Relation-Constant
                                    Function-Constant
                                    Atomic-Term))

(<=> (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)))))))

(<=> (Restricted-Constraint-Term ?Term
                                 ?Class-Of-Term-Operators
                                 ?Class-Of-Object-Constants)
     (And (Term ?Term)
          (Subclass-Of ?Class-Of-Term-Operators Function-Constant)
          (Subclass-Of ?Class-Of-Object-Constants Atomic-Term)
          (Or (Instance-Of ?Term ?Class-Of-Object-Constants)
              (Exists 
                  (?Oper @Args)
                  (And (= ?Term (Listof ?Oper @Args))
                       (Instance-Of ?Oper ?Class-Of-Term-Operators)
                       (=> (Item ?Arg (Listof @Args))
                           (Restricted-Constraint-Term 
                               ?Arg
                               ?Class-Of-Term-Operators
                               ?Class-Of-Object-Constants)))))))