# G4ip

## Описание

Реализация прувера для интуиционистского пропозиционального исчисления G4ip на Haskell.

Форк [cacay/G4ip](https://github.com/cacay/G4ip/)

### Правила вывода

![G4ip rules](g4ip.png)

## Улучшения по сравнению с оригинальным кодом

* деревья вывода строятся явно
* добавлен парсер формул
* добавлен экспорт в LaTeX

## Структура файлов

* G4ip/Proposition.hs   -- Тип данных для формул
* G4ip/Prover.hs -- Прувер
* G4ip/Parser.hs  -- Парсер для формул
* G4ip/LaTeXExporter.hs -- Экспорт в LaTeX

## Использование

```
g4ip [OPTIONS] PROPOSITION
g4ip [OPTIONS]
```

Если формула не указана, пользователю будет предложено ввести её.

### Аргументы командной строки

```
--proof-header <file>       Файл-шаблон для вывода доказательства в LaTeX-нотации - часть, которая будет вставлена в файл до начала prooftree.
                            Значение по умолчанию: static/proof-header.txt
--proof-footer <file>       Файл-шаблон для вывода доказательства в LaTeX-нотации - часть, которая будет вставлена в файл после prooftree.
                            Значение по умолчанию: static/proof-footer.txt
--context-header <file>     Файл-шаблон для вывода контекста - часть, которая будет вставлена в файл до начала списка именованных контекстов
                            Значение по умолчанию: static/context-header.txt
--context-footer <file>     Файл-шаблон для вывода контекста - часть, которая будет вставлена в файл после списка именованных контекстов
                            Значение по умолчанию: static/context-footer.txt
--proof-file <file>         Имя файла для вывода доказательства. Если файл существует, он будет перезаписан.
                            Значение по умолчанию: output/proof.tex
--context-file <file>       Имя файла для вывода списка именованных контекстов. Если файл существует, он будет перезаписан.
                            Значение по умолчанию: output/context.tex
```

### Cинтаксис формул:

```
Пропозициональные переменные - слова из строчных букв английского алфавита и цифр.
Логические связки (после запятой указан приоритет оператора):
  ~ , -    - отрицание, 1
  /\, &    - конъюнкция, 2
  \/, |    - дизъюнкция, 3
  ->, =>   - импликация, 4
  <-, <=   - импликация, 4
  <->, <=> - эквиваленция, 5
Логические константы:
  T - истина
  F - ложь
```

### Конвертация в PDF

Используйте [bussproofs](http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/) и [pdflatex](https://www.tug.org/applications/pdftex/).