Learn Shen
Community Wiki
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.

The Language of Lambda

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 second-order logic. The particular logic used here is called Llambda.

The Language of Llambda


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).


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, composed of a recognised symbol f followed by terms t0, 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, 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.