Index

, , , ,

LONG

refine_using_prl_rule

THEN tactical

REPEAT tactical

ORELSE tactical

refine_using_prl_rule

COMPLETE tactical

cases tactic

bring_hyp tactic

mark tactic

copy tactic

refine_using_prl_rule

THEN tactical

THENL tactical

ORELSE tactical

REPEAT tactical

COMPLETE tactical

PROGRESS tactical

mark tactic

copy tactic

Principia Mathematica

Principia Mathematica

-convertible

archive

atom ,

atom_eq , ,

axiom , ,

cand

check , ,

create ,

decide

delete

dom

dump ,

elim

eval ,

exit ,

fst

ind , ,

inl ,

inr ,

int

int_eq , , ,

intro

jump

KILL

less , ,

list ,

list_ind , , ,

load ,

mod

move ,

new

nil ,

over ,

PULL

PUSH

rec

rec_ind

reduce

scroll ,

shell

SIZE

snd

spread , , , , , , ,

term_of , , , ,

using

view ,

void

tactic

tactical

achieving a subgoal

Ada ,

algebraic structures

Algol--like languages

Algol 68 ,

almost true

argument places of canonical terms

arith rule ,

array definition ,

arrays

arrow keys

artificial intelligence

assertion

associativity ,

associativity defined

assumption ,

assumption list ,

atomic types ,

atom rules

auto--tactic , , , ,

automated theorem proving ,

AUTOMATH , , , ,

AVID ,

backslash character

BAD ,

base case

beta reduction

bindings

bindings in recursive types

booleans ,

bound variables , ,

bracket mode ,

Brouwer ordinals

building theories

call--by--name

canonical members ,

canonical rules

canonical terms , , , , ,

canonical types

canonical value

capture

cardinality ,

carrier set

cartesian product , , ,

case analysis

checking library objects ,

checking ML objects ,

classical logic , ,

classical logical operators

closed ,

closed term

closing windows ,

command language , ,

command module

commands

compact intervals

compiler ,

COMPLETE , ,

complete proof

composition of groups

computable function

computation

computational content , , , ,

computation rules , , , ,

computation system

conclusion , , ,

concurrency

conditional and

conjunction ,

consequent

constructions

constructive analysis

constructive denotational semantics

constructive interpretation of logic

constructive logic , ,

constructive proofs ,

continuity on compact intervals

contractum , ,

control keys

copying text ,

Cornell Program Synthesizer , , ,

CST

cumulative ,

cumulativity rule ,

cursor , , ,

cursor motion

decidable

decision procedure ,

decision terms

declaration , ,

definition display

definitions , , , ,

def rule

delete key

deleting definitions ,

denotational semantics

dependent function , , , , ,

dependent product , , , ,

direct computation

direct computation rules ,

discrete type ,

disjoint union , , ,

disjunction , ,

domain predicate

domain theory

edit window

elim timing

empty list ,

empty type

equal canonical types

equalities as types

equality , , , , ,

equality of types , , ,

equality rule

equality rules ,

equipollent ,

equivalence relation

evaluation , , , , , ,

evaluator , , ,

evaluator bindings ,

excluded middle ,

existence

existential quantification ,

expert reasoners ,

explicit intro rule

expression, readable

extensional

extensionality

extraction , , , , , ,

extraction forms ,

extract term , ,

finite interval

finite precision real type

finite type

formation rules

foundational theory ,

Franz Lisp ,

free variables , , , ,

functional abstraction

functional composition

functionality

functional programming ,

functional programming language

function application ,

function argument

function evaluator

function rules

functions ,

functions|...|computable

functions|...|dependent , ,

functions|...|partial , , , ,

functions|...|respecting equality

functions|...|total ,

goal ,

group theory definitions

header line

head function , ,

head reduction ,

Heyting arithmetic

hidden hypotheses

hiding information ,

hypothesis , , ,

hypothesis list , , ,

hypothesis rule

identity on groups

identity tactic

if--then--else ,

implication , , ,

implicit term construction ,

impredicative

INCOMPLETE , ,

incomplete proof , ,

indexed product

induction

induction form ,

inductive type constructor

inductive type rules

inference rules

infix form

informal argument ,

information hiding

inhabitation , , ,

inhabiting object

initial goal

inject left

inject right

instantiating a some

instantiating definitions

integer induction

integer order relations

integer propositional forms

integer rules

integers ,

intelligent system , ,

interactive environment

interactive medium

intervals of integers

Intuitionism , ,

judgement , , ,

keypad ,

kill buffer , ,

kill key

lambda calculus , ,

lambda expressions

lambda notation

lambda term ,

large types

lazy reduction strategy ,

lazy type constructor

LCF , ,

lemma application tactics

lemma rule ,

less--than for reals

less rules

library , , ,

library commands

library module

library object ordering

library objects

library status ,

library window , ,

linear resolution

list induction ,

list rules

list theory examples

logical operators

macros

main goal

material implication

mathematics libraries

mechanized reasoning

membership , , ,

membership tactic ,

metalanguage , ,

miscellaneous rules

ML , , , , , ,

ML|...| show_auto_tactic

ML|...| set_auto_tactic

ML|...| loadt

ML|...| compilet

ML|...| show_auto_tactic

ML|...| let

ML|...| conclusion

ML|...| refine

ML|...|base types

ML|...|bindings

ML|...|constant terms

ML|...|constructors , , ,

ML|...|declarations

ML|...|destructors , , ,

ML|...|equality

ML|...|exception handling ,

ML|...|expression evaluation ,

ML|...|extensions for

ML|...|functions ,

ML|...|interpreter

ML|...|library objects

ML|...|logical expressions

ML|...|polymorphic type discipline ,

ML|...|predicates

ML|...|prompt ,

ML|...|proof type

ML|...|recursive data types ,

ML|...|recursive functions

ML|...|refinement functions

ML|...|semantics

ML|...|similarities to

ML|...|substitutions

ML|...|syntax ,

ML|...|system use ,

ML|...|tactics

ML|...|term representation

ML|...|tokens and terms

ML|...|type of tactics

ML|...|types , ,

ML|...|types for

ML|...|unification

ML|...|validations ,

modulus of continuity

motion within a proof tree

mouse , ,

mouse cursor

mouse mode

mouse pointer

moving text

negation

negative integer

new clause

noncanonical rules

noncanonical terms , , , , ,

normal--order evaluation

number theory

number theory example

object language , ,

operator precedence ,

outermost redex

outermost reduction

pair constructor , ,

partial function space constructor

partial functions , , , ,

partial type rules

Pascal ,

Peano arithmetic

Pebble

performance degradation

pigeon--hole principle

pigeonhole principle

PL/CV , , ,

PL/I

positioning windows ,

precedence

predefined tactics

predicate calculus

primitive recursion

primitive recursive function

principal argument

product rules

programming|...|constructs

programming|...|environment

programming|...|logic ,

programming|...|methodology

programming|...|ML

programming|...|modes

programming|...|specifications ,

programming|...|synthesis

program verification

PROLOG

prompt modes

prompts ,

proof checking

proof cursor

proof editor , , , , , ,

proof map

Proof Refinement Logic

proof rules

proofs , , ,

proof status

proof status indicators

proof tactics ,

proof tree ,

propositional formulas

propositional functions

propositions as types , , , , , , , ,

quotient

quotient/elim

quotient/equality

quotient/formation

quotient/intro

quotient types , , , , ,

rational approximations

rationals

RAW ,

readable expression

readable text

real analysis

realizability

real numbers

real root--finding program

record constructor

rec rules

recursive definition ,

recursive propositions ,

recursive types , , ,

red ,

redex , ,

reduction rules ,

reduction strategy

refinement

refinement editor , , ,

refinement logic

refinement rules

refinement tactics , , ,

regular sets

relative precedence

remainder theorem

right--click

rule application , , ,

rule categories

rule constructors ,

rule destructors ,

rule format

rule parameters

rules of proof

Russell

saving results ,

selecting text

semantics , ,

sequence

sequence of reals

sequence rule , ,

sequent calculus

sequents , , , ,

set rules ,

set theory ,

set type equality

set types , , , , , , , ,

showing proof text

Simula 67

simultaneous substitution , ,

sizing windows ,

snapshot

square

square root , ,

squash operator , ,

starting up the system

status mark , , , , , , , , ,

stream of states

structure constructor

structure editor

subgoals , ,

subsets

subsets of integers

substitution rule

subtypes , ,

suspend character

Symbolics Lisp

Symbolics Lisp Machine ,

syntax

system description

system performance degradation

T-trees ,

tacticals ,

tactic examples

tactics , , , , ,

tactic writing

tactic writing guidelines

tagged terms

tail function , ,

terminal usage

terms ,

text editor , , , , , , ,

text trees ,

theories

top--down construction ,

total functions ,

transfinite types

transformation tactics , , , , ,

tree cursor

tree position

trichotomy

trivial monotonicity

true sequent ,

turnstile , ,

type constructors ,

typed lambda calculus

type equality , ,

type expression

type functional ,

types , ,

type system

type theory , ,

typing

typing text ,

union, discriminated

union rules

universal quantification ,

universe rules

universes , , , , , ,

UNIX ,

variant record in Pascal

vel

void rules

well--formedness , ,

well--formedness subgoals

well--formedness theorems

well--founded trees

window adjustment , ,

window command menu

window elision

window manager

window of proof editor

windows ,

window system

witness introduction

Zetalisp