Index

abort

answer extraction , , ,

Ask on Failure?

Ask when Dump Proof?

Assume Hypothesis Consistent?

Assume imported conjectures are theorems?

Assume preceding local conjectures are theorems when proving a conjecture?

axiom

axiom

sort ,

translation of , ,

axiom list , , , ,

backward

Backward Depth Limit

Backward Derivation Limit

backward inference phase

Backward Interact?

bag , ,

Choice of Dump Proofs

circularity

col

colimit

collection , ,

collection

empty

conjecture , , ,

conjectures

subset of , ,

Conjectures to Focus

conservation theorem, for sacks

constructor function

constructor set ,

customize

decomposition theorem, for collections

default

deomposition theorem, for collections

Display/modify Specware Proof Options ,

Display Backward Derivations?

Display Forward Derivation?

Display Input Clauses?

Display Proof Object?

Display Proof Tree?

Display Sort Axioms?

Display Type Constraints?

do it

empty-col

Enforce Strong Dependency?

forward

Forward Depth Limit

Forward Derivation Limit

Forward Fnsnest Limit

forward inference phase

Forward Interact?

free paramodulation

Generic Forward Inference?

ignore ,

Ignore Data Types?

Ignore following local theorems when proving a conjecture?

import , ,

Include Sort Axioms?

induction , , , ,

insert-b-as-s

insert-col ,

interpretation ,

joke

KITP , , ,

left-to-right ,

Maximum Input Clauses

Maximum New Variables

mediator

Minimum Witnesses Deduced

morphism , , , ,

O-F (strategy)

paramodulation ,

permutation ,

postponed verification , ,

prenex normal form required

prepend

project

prover options

resolution

retention theorem, for sacks

Return Value when Fail

rewrite ,

rewriting

right-to-left ,

sack

sample sessions

saving proofs ,

Search Strategy

Select an Operation

Select an Operation ,

Select Conjectures to verify?

Select Conjectures to Verify?

Select Witnesses by:

sequence ,

set ,

Set KITP prover options?

Set KITP prover options?

Set New Values for Prover (Kitp) Parameters

set of support

Set Problem-set Directory

Set Prover Display Options , ,

Set SPECWARE Parameters

Set Specware Proof Options , ,

simplification

sort axioms ,

source

specification ,

specification

import of

translation of ,

Specify induction tactics?

Specify induction tactics?

Specify Proof Directives

Specify proof directives for?

Specify Proof Tactic

Specify prover usage of Spec axioms/theorems:

Specify theorem usage as default

strategy , , , ,

subset of conjectures , ,

Suppress KITP Message?

target

theorem

translation

of axiom ,

of axioms

of specification ,

type ,

uniquesness axiom, for bags

Use Default Specware Proof Options

Use Free Paramodulation?

Use Typed Inference

Verify parsed theorems?

Verify parsed axiom translation?

Verify parsed axiom translation

Verify Parsed Theorems?

When prover fails, query user to accept theorems anyway?