ProofChecker

Program do sprawdzenia poprawności dowodów formuł logicznych w systemie dedukcji naturalnej.

Wprowadzone rozszerzenia:

• Obsługa formuł I rzędu
• Możliwość korzystania z aksjomatów
• Możliwość korzystania z udowodnionych formuł
• Obsługa arytmentyki pierwszego rzędu
• Informacja o lokalizacji i rodzaju błędu
• Automatycznie wypełnianie dziur
• Generowanie drzew dowodu za pomocą termów rachunku lambda

Więcej informacji w dokumentacji programu oraz w instrukcji obsługi aplikacji.

Kompilacja:

ocamlbuild -I rules -use-menhir -tag thread -use-ocamlfind -quiet -pkg core main.native

Testowanie:

./main.native test.txt lub ./main.native test.txt >> log_file 2>> err_file

Gramatyka:

• program -> definition | definition_program
• definition ->
  | goal label : expression proof natural_deduction end.
  | proof natural deduction end.
  | axiom expression.
  | type label ( ) = type_name.
  
• natural deduction ->
  | natural_deduction ; proof
  | proof
  
• proof ->
  | [ premise : natural deduction ]
  | [ [ var ] , expression : natural deduction ]
  | [ [ var: type_name], premise: natural_deduction ]
  | [ [ var: type_name]: natural_deduction ]
  | [ [ var ] : natural_deduction ]
  | expression
  
• premise -> expression
  
• expression ->
  | term = term
  | expression <=> expression
  | expression => expression
  | expression \/ expression
  | expression /\ expression
  | ~ expression
  | var (term)
  | var
  | (expression)
  | T
  | F
  | V var. expression
  | V var : type_name . expression
  | E var. expression
  | E var : type_name . expression
  
• term -> term,var | var
  

var - dowolnej długości ciąg znaków zaczynający się od małej litery
type_name - dowolnej długości ciąg znaków zaczynający się od dużej litery
V - Kwantyfikator ogólny
E - Kwantyfikator egzystencjalny