OK. You have a marvelous looking
webpage. On this you want to share some nice proofs. Maybe you have used BoxProver as assistant. Now it sounds like the app you need is this.

I have made some changes to the grammar - these are described in the "Syntax" section. A line can be followed by a line, no naming are needed. Name tokens can be created using "" - that is anything that is not " goes in here. I have made it so that implication can be written both as => or ->.

Now this put together you can make proofs either by copying the whole boxproof from BoxProver apart from the head, that is the

%abbrev
d : {S}{Q}{x_1} proof ( S => exi ([x] Q x) , |- exi ([x] S => Q x) ) =
[S][Q][x_1]

part. Or you can create arbitrary proofs in a simpler way:

"I <3 deduction" premise
p premise
q \/ ~q by lem
(
q assumption
(
q assumption
p by copy 1
)
p -> q by imp_i "5 - 7"
)
(
~q assumption
(
q assumption
bot by neg_e 10 11
p by bot_e 12
)
q => p by imp_i "10 - 14"
)
q -> p by dis_e 2 "10-14" "13-17"

Note that keywords like "lem" must be followed by a space for the lexer to recognize it.

Back to your nice looking homepage. You can find the git repo here. Grap the file boxproofs.js. Insert the code of stack.js into somewhere reachable. boxproofs.js is a 8000 loc file. This can be a bit overwhelming. However, in order to change the appearance of the boxes you have to change within the object var html found near line 7572. In this you can style the container, the lines and even the error messages.

Finally create spans with boxproves, say you name the class "boxproof". Now run:

var bproofs = new BoxProofs();
bproofs.createBoxesHtml(document.getElementsByClassName("boxproof"));

Feel free to tinker around. As goes for most of these projects, this isn't copyrighted.

And if you find any errors - that is proofs accepted by boxprover, but not this app, please make a comment below on the problem.

CommentsGuest Name:Comment:

[Untyped_Lambda_Calculus] Untyped Lambda Calculus in JavaScript;;Default.aspx?id=31;;;;[Untyped_Lambda_Calculus] Parser;;Default.aspx?id=32;;;;[Untyped_Lambda_Calculus] Semantics;;Default.aspx?id=35;;;;[Untyped_Lambda_Calculus] Evaluation;;Default.aspx?id=33;;;;[Untyped_Lambda_Calculus] Testing;;Default.aspx?id=34;;;;[Untyped_Lambda_Calculus] Usage;;Default.aspx?id=36;;;;[BoxProver] BoxProver - Intro;;Default.aspx?id=27;;;;[BoxProver] BoxProver - Syntax;;Default.aspx?id=28;;;;[BoxProver] BoxProver - HTML usage;;Default.aspx?id=29;;;;[BoxProver] BoxProver - Latex usage;;Default.aspx?id=30;;;;[Grammar2Slr] Parser Generator - Intro;;Default.aspx?id=23;;;;[Grammar2Slr] Parser Generator - Syntax;;Default.aspx?id=24;;;;[Grammar2Slr] Parser Generator - Definitions;;Default.aspx?id=25;;;;[Grammar2Slr] Parser Generator - Workings;;Default.aspx?id=26;;;;[Prop2Table] Proposition to Table - Preface;;Default.aspx?id=13;;;;[Prop2Table] Proposition to Table - Parsing input (SLR parser);;Default.aspx?id=14;;;;[Prop2Table] Proposition to Table - Parser F# code;;Default.aspx?id=15;;;;[Prop2Table] Proposition to Table - Well-formed syntax;;Default.aspx?id=16;;;;[Prop2Table] Proposition to Table - Semantics of propositional logic;;Default.aspx?id=17;;;;[Prop2Table] Proposition to Table - Constructing tables;;Default.aspx?id=18;;;;[Prop2Table] Proposition to Table - The application;;Default.aspx?id=19;;;;[Grammar2Set] Grammar to Set - Preface;;Default.aspx?id=6;;;;[Grammar2Set] Grammar to Set - Syntax of Input;;Default.aspx?id=7;;;;[Grammar2Set] Grammar to Set - Nullable;;Default.aspx?id=8;;;;[Grammar2Set] Grammar to Set - First;;Default.aspx?id=9;;;;[Grammar2Set] Grammar to Set - Follow;;Default.aspx?id=10;;;;[Grammar2Set] Grammar to Set - The Application;;Default.aspx?id=11;;;;[Nfa2Dfa] NFA to DFA convert - Preface;;Default.aspx?id=2;;;;[Nfa2Dfa] NFA to DFA convert - Syntax/Input;;Default.aspx?id=3;;;;[Nfa2Dfa] NFA to DFA convert - Convertion;;Default.aspx?id=4;;;;[Nfa2Dfa] NFA to DFA convert - The Application;;Default.aspx?id=5;;;;[Nfa2Dfa] NFA to DFA convert - Version 1.1;;Default.aspx?id=12;;;;[ComCalc] Simple Calculator - Preface;;Default.aspx?id=1;;;;[ComCalc] Simple Calculator - Syntax;;Default.aspx?id=20;;;;[ComCalc] Simple Calculator - Generating parser;;Default.aspx?id=22;;;;[ComCalc] Simple Calculator - The application;;Default.aspx?id=21;;;;