# 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.