Message Boards Message Boards

1 Reply
1 Total Likes
View groups...
Share this post:

Implement Sequent calculus into mathematica

Posted 10 years ago

Is it possible to implement a Sequent calculus of first order mathematical Logic into mathematica an manipulate expressions of the first order mathematical language?
The calculus would consits of 9 rules that tell mathematica which changes can be made on a certain expression written in the first order language.

For example there would be a rule like

which means that if there is a expression like

mathematica ist allowed to manipulate it by deleting the quantifier and the variable and get the solution
POSTED BY: Nickel Paulsen
Is it possible to implement this? Yes. (Well it is possible to implement in any programming language, but Mathematica is actually a good choice, which is what really matters). Mathematica/The Wolfram Language excels at describing symbolic transformations and typsetting different notations. But what features are you looking for? If you look online a bit, it looks like there's implementations in COQ, which would be useful for theorem proving. I don't know what you intend to do. 

The first thing to do is to implement sequent calculus using ordinary expressions. After that, you can use the Notation package in Mathematica to create the kind of typesetting you want. To begin with, I'd read thru the Mathematica virtual book to get a feeling for how to program in Mathematica. After that, take a look at the Notation package in the documentation. 
POSTED BY: Sean Clarke
Reply to this discussion
Community posts can be styled and formatted using the Markdown syntax.
Reply Preview
or Discard

Group Abstract Group Abstract