Professional
Home
Learn Shen
Videos
Community Wiki
Community
OS Kernel
OS Library
Shen
Professional

The Shen
Logic Lab: Shilbert
This is a portal for help
in learning about components of the Shen Logic
Lab. The logic lab
is a cloud based system which is maintained over
the web; as with all SP components you do not
have reinstall updates which flow into the system
month by month. This page deals with
Shilbert; a program that converts Shen programs
into typed second order logic. This program sits
in the shilbert package.


Shilbert is loaded into
SP by the Shilbert plugin. You'll end with a toolbar with
two options (resume is under development).
If you click on render then you'll be presented with a
window inviting you to load a file into Shilbert. This
file should be a type secure Shen program (i.e. one with
types). If you choose a file myfile.shen, Shilbert will load it and then
produce the file myfile.shen.axioms. with a message similar to
28 axioms
generated in 2539 inferences
run time: 0.0149993896484375 secs
This file will contain a
rendering of your program into typed secondorder logic.
The particular logic used here is called Llambda.
The
Language of Llambda
Types
1. boolean : type, symbol : type,
string : type, nn : type (natural number) and type :
type.
2. If A and B are types so is (list A) and (A * B) and (A
> B).
Wffs
1. A logical constant is v, ~, &, =>, <=>, all, =, :, type, lambda.
2. A recognised symbol is a symbol other than a logical
constant.
3. A recognised symbol or a string or a boolean or a
natural number is a term. So is (lambda x t) where x is a recognised
symbol and t is a term.
4. A function application (f t0,...tn) composed of a
recognised symbol f followed by terms t0,...tn of type A0
> ... An > An+1 ... Ao is itself a term of type
An+1 ... Ao if it is provable that every ti inhabits the
type Ai.
5. A predicate is a recognised symbol.
6. An application composed of a predicate of type A0 ...
An > boolean followed by terms t0,...tn of type A0
> ... An is an atom.
7. If T and T' are terms of type A then (T = T') is an atom.
8. An atom is a wff.
9. A type (expression) is a term.
10 A typing (X : T) where X is a term and T is a type is
a wff.
11. If P and Q are wffs, A is a type expression and V is
a recognised symbol then (~ P), (P v Q), (P & Q), (P => Q), (P <=> Q), (all V : A P) are wffs.
This program is a component of a
larger system to be discussed in publication; the program
is included here for interest.
