sequents

KO | EN

gitlite — search

#python #java #python3 #arduino #golang #machine-learning #rust #html #flask #javascript #seismology #nodejs

★ 27 Open GitHub ↗

Proof search for intuitionistic propositional logic using Dyckhoff's LJT.

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# sequents [![Build Status](https://travis-ci.org/ayberkt/sequents.svg?branch=master)](https://travis-ci.org/ayberkt/sequents)

**sequents** is an implementation of [Roy Dyckhoff's LJT](https://www.jstor.org/stable/2275431)—a sequent
calculus for intuitionistic logic that is decidable and does _not_ need loop
checking

## Building

First make sure that you have `smlnj` installed. To build, run
```
./script/build.sh
```

## Trying out

Let's prove the commutativity of conjunction `A ∧ B ⊃ B ∧ A`. Using the ASCII
approximations of the connectives, we can pipe this proposition into `sequents`.
```
➜ echo "A /\ B => B /\ A" | ./sequents
```
which gives the following:
```
Proof found!
Theorem: A ∧ B ⊃ B ∧ A.
• A, B ----> B by init
• A ∧ B ----> B by ∧L

• B, A ----> A by init
• A ∧ B ----> A by ∧L

• A ∧ B ----> B ∧ A by ∧R
• ----> A ∧ B ⊃ B ∧ A by ⊃R
QED
```

You can also generate LaTeX with `--latex` flag. Make sure that you have `ebproof`
installed though.
```
➜ echo "A /\ B => B /\ A" | ./sequents --latex > out.tex
➜ pdflatex out.tex
```
![derivation](https://raw.githubusercontent.com/ayberkt/sequents/master/resources/derivation.png)

sequents

Explore Similar Repositories

Was this content helpful?

Recent Feedback

Download README