Class Seqvar

Subclass-Of@Frame-Ontology: Variable, Expression, Word
Instance-Of@Frame-Ontology: Class@Frame-Ontology, Relation@Ol-User%Kif-Relations, Set
Arity@Frame-Ontology: 1
Documentation@Ol%Frame-Ontology:
A sequence variable in a KIF expression. For every sequence variable $omega$, there is an axiom asserting that it is a sequence variable. Each such axiom is a defining axiom for the {tt seqvar} relation.


Slots:


Frame References to Seqvar:

In class@frame-ontology Variable:

Exhaustive-Subclass-Partition@Frame-Ontology: {Indvar, Seqvar}

Equivalence Axioms mentioning Seqvar:

(<=> (Quanterm ?X)
     (Or (Exists (?T ?P)
                 (And (Term ?T)
                      (Sentence ?P)
                      (= ?X (Listof 'The ?T ?P))))
         (Exists (?T ?P)
                 (And (Term ?T)
                      (Sentence ?P)
                      (= ?X (Listof 'Setofall ?T ?P))))
         (Exists (?Vlist ?P)
                 (And (List ?Vlist)
                      (Sentence ?P)
                      (>= (Length ?Vlist) 1)
                      (=> (Item ?V ?Vlistp) (Indvar ?V))
                      (= ?X (Listof 'Kappa ?Vlistp ?P))))
         (Exists (?Vlist ?Sv ?P)
                 (And (List ?Vlist)
                      (Seqvar ?Sv)
                      (Sentence ?P)
                      (=> (Item ?V ?Vlist) (Indvar ?V))
                      (= ?X
                         (Listof 'Kappa
                                 (Append ?Vlist (Listof ?Sv))
                                 ?P))))
         (Exists (?Vlist ?T)
                 (And (List ?Vlist)
                      (Term ?T)
                      (>= (Length ?Vlist) 1)
                      (=> (Item ?V ?Vlistp) (Indvar ?V))
                      (= ?X (Listof 'Lambda ?Vlistp ?T))))
         (Exists (?Vlist ?Sv ?T)
                 (And (List ?Vlist)
                      (Seqvar ?Sv)
                      (Sentence ?T)
                      (=> (Item ?V ?Vlist) (Indvar ?V))
                      (= ?X
                         (Listof 'Lambda
                                 (Append ?Vlist (Listof ?Sv))
                                 ?T))))))