Главная    Ex Libris    Книги    Журналы    Статьи    Серии    Каталог    Wanted    Загрузка    ХудЛит    Справка    Поиск по индексам    Поиск    Форум   
Поиск по указателям

Gordon X. — Edinburgh LCF: A Mechanized Logic of Computation
Gordon X. — Edinburgh LCF: A Mechanized Logic of Computation

Читать книгу

Скачать книгу с нашего сайта нельзя

Обсудите книгу на научном форуме

Нашли опечатку?
Выделите ее мышкой и нажмите Ctrl+Enter

Название: Edinburgh LCF: A Mechanized Logic of Computation

Автор: Gordon X.


Edinburgh LCF is a computer system for doing formal proofs interactively. This book is both an introduction and a reference manual for the complete system (and its DECsystem-10 implementation). The acronym LCF stands for "Logic for Computable Functions" - a logic due to Dana Scott in which facts about recursively defined functions can be formulated and proved. The original system (developed at Stanford University) was a proof checker for this logic, based on the idea not of proving theorems automatically, but of using a number of commands to generate proofs interactively step by step. The emphasis then was on exploring the class of problems that could conveniently be represented in the logic, and on discovering the kinds of patterns of inference that arose when solving these problems. It was found that, by and large, the original logic was expressive enough, although a few useful extensions were suggested. However, the fixed repertoire of proof-generating commands often required long and very tedious interactions to generate quite simple proofs; furthermore these long interactions often consisted of frequent repetitions of essentially the same sequence of inferences.

Язык: en

Рубрика: Computer science/

Статус предметного указателя: Готов указатель с номерами страниц

ed2k: ed2k stats

Год издания: 1980

Количество страниц: 159

Добавлена в каталог: 05.12.2010

Операции: Положить на полку | Скопировать ссылку для форума | Скопировать ID
Предметный указатель
$#      A6a
$*      A3b
$+      A3b
$-      A3b
$.      A3b
$/      A3b
$<      A3b
$=      A3b
$>      A3b
$@      A3b
$do      A3b
$not      A3b
$o      A6a
$ORELSE      A9.3
$THEN      A9.3
$THENL      A9.3
abs      A5.2c
aconvform      A7f
aconvterm      A7f
admitsinduction      3.3
ANAL      A5.2a
APTERM      A5.2b
APTHM      A5.2b
assoc      A6b
assume      A5.1a
AXDEF      A5.2f
Axiom      3.4.2 3.4.3
AXTRUTH      A5.1a
BASICSS      A8 A8.4
BETACONV      A5.2c
Can      A6a
cases      A5.2f
CASESTAC      A9.2
combine      A6d
concl      A7c
CONDCONV      A5.2f
CONJ      A5.1b
contr      A5.2f
DEFCONV      A5.2f
DEFUU      A5.2f
destabs      A4.2
destcomb      A4.2
destcond      A7d
destconj      A4.3
destconst      A4.2
desteguiv      A4.3
destimp      A4.3
destineguiv      A4.3
destpair      A7d
destquant      A4.3
destthm      A4.4
desttruth      A4.3
desttype      A4.1
destvar      A4.2
destvartype      A4.1
DISCH      A5.1b
Dot      A5.2g
DOWNCONV      A5.2h
easytype      3.3
ETACONV      A5.2c
EXISTS      A6b
Explode      A3a
Ext      A5.2c
Fact      3.4.2 3.4.3
Filter      A6d
find      A6b
finitetype      3.3
fix      A5.2e
FIXPT      A5.2e
Flat      A6d
FORALL      A6b
formfrees      A7e
formlfrees      A7e
formltyvars      A7e
formlvars      A7e
formmatch      A7j
formtyvars      A7e
formvars      A7e
freeinform      A7f
freeinterm      A7f
FST      A3a
gen      A5.1b
genmem      A6b
GENTAC      A9.2
gentok      A3a
genvar      A7e
HALF1      A5.2a
HALF2      A5.2a
HD      A3a
HYP      A7c
i      A6a
IDTAC      A9.3
implode      A3a
INCONV      A5.2j
INDUCT      A5.2e
INDUCTAC      A9.2
inl      A3a
inr      A3a
INST      A5.1d
instinform      A7h
instinterm      A7h
instintype      A7h
INSTTYPE      A5.1d
intersect      A6d
intoftok      A3a
isabs      A7a
iscomb      A7a
isconj      A7a
isconst      A7a
ISCONV      A5.2j
isequiv      A7a
isimp      A7a
isinequiv      A7a
ISL      A3a
isquant      A7a
istruth      A7a
isvar      A7a
isvartype      A7a
itlist      A5c
K      A5a
LAMGEN      A5.2b
Length      A6e
lhs      A7c
maketheory      3.4.3
MAP      A6c
mapfilter      A6d
MEM      A6b
MIN      A5.2d
MINAP      A5.2d
MINFN      A5.2d
mkabs      A4.2
mkcomb      A4.2
mkcond      A7d
mkconj      A4.3
mkconst      A4.2
mkequiv      A4.3
mkguant      A4.3
mkimp      A4.3
mkinequiv      A4.3
mkpair      A7d
mktruth      A4.3
mktype      A4.1
mkvar      A4.2
mkvartype      A4.1
mlcinfix      A3a
mlin      A3a
mlinfix      A3a
MP      A5.1c
nametype      3.4.3
newaxiom      3.4.3
newconstant      3.4.3
newfact      3.4.2 3.4.3
newolcinfix      3.4.3
newolinfix      3.4.3
newparent      3.4.3
newtype      3.4.3
NIL      A6e
NULL      A3a
OUTCONV      A5.2j
outl      A3a
outr      A3a
pair      A6a
PAIRCONV      A5.2i
phylumofform      A7b
phylumofterm      A7b
printbool      A3a
printdot      A3a
PrintForm      A3a
printint      A3a
printterm      A3a
printthm      A3a
printtok      A3a
printtype      A3a
REFL      A5.2a
REPEAT      A9.3
rev      A6d
revassoc      A6b
revitlist      A6c
rhs      A7c
SEL1      A5.1c
SEL2      A5.1c
SELCONV      A5.2i
simp      A5.2k
simpform      A8.3
SIMPTAC      A9.2
simpterm      A8.2
SND      A3a
Spec      A5.1c
Split      A6d
ssadd      A8.1
ssaddf      A8.1
ssunion      A8.1
SUBS      A5.2a
SUBSOCCS      A5.2a
subst      A5.2a
SUBSTAC      A9.2
substinform      A7g
substinterm      A7g
substoccsinform      A7g
substoccsinterm      A7g
Subtract      A6d
SYM      A5.2a
Synth      A5.2a
termfrees      A7e
termmatch      A7j
termtyvars      A7e
termvars      A7e
TL      A3a
tokofint      A3a
Trace      A10
Trans      A5.2a
tryfind      A6b
typemode      A7i
typeof      A7c
typesinform      A7f
typesinterm      A7f
typesintype      A7f
typetyvars      A7e
union      A6d
untrace      A10
UPCONV      A5.2h
Variant      A7e
       © Электронная библиотека попечительского совета мехмата МГУ, 2004-2017
Электронная библиотека мехмата МГУ | Valid HTML 4.01! | Valid CSS! О проекте