The language Maude provides simple implementation tools of proof construction and proof search for CoS systems. However, using these tools requires (minor) knowledge of the language Maude, and also the output generated by these tools is remote from the usual CoS syntax.
The goal of this project is providing a simple user-friendly interface to these Maude modules which would make it possible to use the tools interactively: this way, the user can guide the proof construction and choose between automated proof search and user-guided proof construction. Then, by using the LaTeX macros in-hand, the output derivation can be generated as a user-friendly, dvi file, as in the papers on deep inference.
While a simple implementation can be accomplished within a weekend by an experienced programmer who has a deep understanding of the CoS systems and the Maude implementation tools, a sophisticated implementation is well suited as a project task.
The switch rule of system KS is responsible for the context management in proof construction. However, also due to its deep applicability, this rule brings a great redundant nondeterminism in proof search. The system KSi of the calculus of structures is obtained by replacing the switch rule in system KS with the rule lazy interaction switch (lis). The rule lis allows the goal directed instances of the switch rule with respect to proof construction. System KSi is complete for classical logic and because of deep inference, as system KS, it brings shorter proofs than in, e.g., the sequent calculus.
In this project, a proof search implementation of this system has to be developed. This implementation should allow experimenting with different search strategies such as 'prior-deep instances of the inference rules' while keeping the contraction rule under control.
Development of a tool which implements the results on decomposition of the proofs and cut-elimination. This project can be accomplished by first establishing an appropriate data structure for representing derivations, and then by using the proofs of the permutation, decomposition and cut-elimination results as algorithms.
Ideally, this tool should be modular in the sense that it can be composed with the Maude implementations.
Establishment of a formal relationship between SKS proofs and proofs constructed in connection method is the topic of this project. This project requires a deep understanding of the system SKS and the classical logic proofs in connection method. As a warm-up for this project the student can first investigate the relationship between the multiplicative linear logic proofs in the CoS and the Linear Connection Method.
Formalisms A and B are "bureaucracy-free" generalizations of the formalism of the calculus of structures. Proofs in these formalisms are parallelized derivations which can be considered as concurrent computations.
In this project, an algorithm which extracts a normal form of a CoS proof with respect to formalisms A and B should be established and implemented.