The aim of the project is to describe proof-theoretically, and implement in the functional programming language (Haskell), complex deductive systems containing various proof systems as modules. The systems are called distributive deductive systems, as they contain functions which allow to distribute costs of a derivation among various modules. The description is to be gained for a wide range of logics. The next target will be to conduct a series of computational experiments and analyses the results of which will be used to improve the structure and computational complexity of the existing proof systems.
The project, funded by National Science Centre, Poland, started in April 2018 (grant no. 2017/26/E/HS1/00127, title in Polish: Dystrybutywne systemy dedukcyjne dla logiki klasycznej i pewnych logik nieklasycznych. Teoria dowodu wspomagana wybranymi metodami obliczeniowymi).
Distributive Deductive Systems 