Previous: AIDA-96-15 Next: AIDA-96-17 Index 1996

Intellectics Group: Technical Report 96-16

Enno Sander

Problem-Oriented Applications of Automated Theorem Proving

This paper provides a unified approach for matrix characterizations for propositional substructural logics, whereby the focus is laid on a uniform representation of different validity concepts in matrices. Starting from a restricted validity concept for matrices called basic-validity, where a matrix is considered as valid if each literal is connected exactly once, we use rewrite rules to obtain a wider class of validity concepts. Here a matrix is considered as valid if it can be transformed to a basic-valid matrix by using the appropriate rewrite-rules. For each validity concept we give corresponding algebraic semantics.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry