Automated Deduction Techniques for Studying Rough Algebras

Article type: Research Article

Authors: Vigneron, Laurent

Affiliations: LORIA – Université Nancy 2, B.P. 239, 54506 Vandœuvre-lès-Nancy Cedex, France. E-mail: vigneron@loria.fr

Abstract: We present a non-exhaustive state of the art in the domain of deduction in first-order logic with equality, describing different strategies introduced over the years: strategies for selecting deduction steps, for eliminating redundant information, for delaying the resolution of unsolved or too difficult problems, for applying deductions with built-in properties. We also present the system daΤac that implements our deduction techniques modulo associative-commutative properties. Finally we detail an application of those techniques to the study of non-classical logics, work realised in collaboration with Prof. Wasilewska (Stony Brook University, New York).

Keywords: automated deduction, theorem proving, equational theories, first-order logic, constraint deduction, modal logic, rough sets

DOI: 10.3233/FI-1998-33105

Journal: Fundamenta Informaticae, vol. 33, no. 1, pp. 85-103, 1998