Representation Theorems and Automated Theorem Proving in Non-Classical Logics

Sofronie-Stokkermans, Viorica

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

Representation Theorems and Automated Theorem Proving in Non-Classical Logics

MPS-Authors

/persons/resource/persons45516

Sofronie-Stokkermans, Viorica
Automation of Logic, MPI for Informatics, Max Planck Society;
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

Sofronie-Stokkermans, V. (1999). Representation Theorems and Automated Theorem Proving in Non-Classical Logics. In Proceedings of the 29th IEEE International Symposium on Multiple-Valued Logic (ISMVL-99) (pp. 242-247). Los Alamitos, USA: IEEE.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-368E-6

Abstract

In this paper we present a method for automated theorem proving in non-classical logics having as algebraic models bounded distributive lattices with certain types of operators. The idea is to use results from Priestley duality for distributive lattices with operators in order to define a class of Kripke-style models with respect to which the logic is sound and complete. If this class of Kripke-style models is elementary, it can then be used for a translation to clause form; satisfiability of the resulting clauses can be checked by resolution. We illustrate the general ideas by several examples, one of which is presented in detail.