WFFOP : wff operation

OTL Object

• match

Printing

• prw

Printing

• display-etree
• display-etree-all
• etree-to-list
• pnode
• pproof
• ppw
• ppwdeep
• pw
• pwdeep
• pwnode
• pwscope
• pwshallow
• pwtypes
• tr-print-etree
• tr-print-etree*
• tr-print-etree-file*

Internal for Printing

• prt-aplicn-p
• prt-associative-p
• prt-infix-op
• prt-prefix-op
• prt-symbol-p

Weak Labels

• create-weak
• delete-weak
• dissolve-weak
• dissolve-weak*
• redef-weak

Saving Wffs

• sv-wff

Recording

• remark-printedtfile
• remark-printmatefile

Expansion Trees

• apply-prim-subs
• apply-prim-subs-all
• apply-prim-subs-outer
• deepen-etree
• deepen-one
• deepen-to-literals
• deepen=
• duplicate-all-outer-vars
• duplicate-all-vars
• expand
• gwff-to-etree-sub
• modify-status
• name-primsubsts2
• prim-single
• sel-exp-terms
• select

Mtree Operations

• add-conn-ob
• mst-go-down
• mst-go-sib
• mst-go-up
• mst-goto
• mst-kill
• mst-resurrect
• pick-lit

Mtree Printing

• mst-conns-added
• pprint-obligation
• pprint-obligation-path
• print-live-leaves
• print-matingstree
• print-matingstree-node
• print-obligation
• print-obligation-jform
• print-obligation-literal
• print-obligation-path
• print-obtree-node
• tr-pobtree
• tr-print-matingstree
• tr-print-matingstree-ob

Mtree Auto

• add-all-lit
• add-all-ob
• expand-mst-leaves
• mst-basic-search
• mst-fewest-ob-search
• mst-lb-search
• query-ob

Mating search

• call-unify

MS88 search procedure

• add-conn
• add-conn*
• apply-substs-ms
• complete-p
• init-mating
• minimal-p
• ms88-sub
• rem-conn
• rem-conn*
• rem-last-conn
• show-mating
• show-substs

Vpforms

• cr-eproof-jform
• cw-deep
• cw-jform
• cw-shallow
• display-vp-diag
• display-vp-diag-ed
• display-vp-etree
• display-vpd
• gwff-to-jform
• gwff-to-prop-jform
• jform-to-gwff
• number-of-horizontal-paths
• number-of-vertical-paths
• print-jlist
• vp-tex
• vpform

wff Primitives

• apply-wff
• bindhead
• binding
• bindvar
• change-print-type
• dupwff
• free-vars-of
• intern-subst
• make-wffschema
• rename-bd-var
• subst-1-type
• substitute-types
• type
• type-of-arg-1

Equality between Wffs

• inmost-gar
• not-wffeq
• wffeq
• wffeq-ab
• wffeq-def
• wffeq-defeq
• wffeq-lnorm
• wffeq-nnf

Predicates on Wffs

• a-bd-wff-p
• abbrev-p
• ae-bd-wff-p
• and-p
• anyabbrev-p
• anypropsym-p
• boundwff-p
• e-bd-wff-p
• equal-type-p
• equals-p
• equiv-p
• free-for
• free-in
• gvar-p
• gwff-p
• implies-p
• infix-op-p
• infix-p
• is-variable
• label-p
• lambda-bd-p
• legal-type-p
• logconst-p
• lsymbol-p
• non-atomic
• non-atomic-or-truthvalue
• not-free-in
• not-free-in-hyps
• not-free-in-wffset
• not-p
• or-p
• pmabbrev-p
• pmpropsym-p
• propsym-p
• r-prime-restr
• reduct-p
• same-modulo-equality
• subst-occs
• subst-some-occurrences
• type-equal
• wff-applic-p

Moving Commands

• find-binder
• find-infix
• find-infix-etree
• gar
• gdr
• glr
• goto-node
• grr
• ntharg
• replace-gar
• replace-gdr
• replace-glr
• replace-grr

Changing Commands

• change-top
• delete-topconn-lscope
• delete-topconn-rscope
• mbed-and-left
• mbed-and-right
• mbed-equiv-left
• mbed-equiv-right
• mbed-existential
• mbed-existential1
• mbed-forall
• mbed-implics-left
• mbed-implics-right
• mbed-lambda
• mbed-or-left
• mbed-or-right
• mbed=left
• mbed=right
• merge-constant
• merge-idempotent
• wff-absorb
• wff-associative-l
• wff-associative-r
• wff-commutative
• wff-dist-contract
• wff-dist-expand
• wff-double-negation
• wff-permute
• wff-sub-equiv
• wff-sub-implies

Recursively Changing Commands

• assoc-l
• merge-constant*
• merge-idempotent*
• wff-absorb*
• wff-associative-l*
• wff-associative-r*
• wff-commutative*
• wff-dist-contract*
• wff-dist-expand*
• wff-double-negation*
• wff-permute*
• wff-sub-equiv*
• wff-sub-implies*

Rewriting commands

• apply-rrule-1
• apply-rrule-1*
• apply-rrule-any
• apply-rrule-any*
• create-rewrite-rule
• instance-of-rewriting
• simplify-down
• simplify-down*
• simplify-up
• simplify-up*
• unapply-rrule-1
• unapply-rrule-1*
• unapply-rrule-any
• unapply-rrule-any*

Substitution

• do-primsub
• duplicate-var
• instantiate-binder
• replace-equiv
• replace-equiv-all
• s
• subst-some-occs
• substitute-in-etree
• substitute-l-term-var
• substitute-term-var
• wff-identity

Basic Abbreviations

• abbr-list
• const-list
• contains-defn
• inst-def
• instantiate-1
• instantiate-all
• instantiate-defn
• instantiate-equalities
• instantiate-top-equality
• lib-abbr-list
• new-defs
• rpin
• substitute-bdvar-scope
• top-level-defn

Lambda-Calculus

• ab-change
• ab-normal-p
• ab-normalize
• eta-exp
• eta-to-base
• etacontr
• etanorm
• lambda-norm
• lcontr
• lexpd
• lnorm
• lnorm-beta
• lnorm-eta
• long-eta
• rewrite-all-equivalence
• untyped-lambda-norm
• wffeq-ab-beta
• wffeq-ab-eta
• wffeq-ab-lambda

Negation movers

• neg-norm
• negwff
• pull-negation
• push-negation

Primitive Substitutions

• name-primsubsts
• primsubsts

Miscellaneous

• clause-form
• conjunctive-normal-form
• find-subformulas
• head
• hvars
• min-quant-scope

RuleP

• sat-p
• valid-p

Skolemizing

• simul-substitute-l-term-var
• skolems1
• skolems3

Quantifier Commands

• delete-binder
• delete-leftmost-binder
• openwffa
• openwffe

Wellformedness

• culprit-p
• find-culprit
• locateunwffs

Statistics

• delete-duplicate-conns
• show-mating-stats

TPS documentation homepage

TPS homepage