Building Automated Theorem Provers for Infinitely-Valued Logics with Satisfiability Modulo Theory Solvers

There is a relatively large number of papers dealing with complexity and proof theory issues of infinitely-valued logics. Nevertheless, little attention has been paid so far to the development of efficient solvers for such logics. In this paper we show how the technology of Satisfiability Modulo The...

Full description

Saved in:
Bibliographic Details
Main Authors: Ansótegui, C., Bofill, M., Manyà, F., Villaret, M.
Format: Conference Proceeding
Language:English
Subjects:
Benchmark testing
Buildings
Calculus
Cognition
Complexity theory
Encoding
Fuzzy logic
infinitely-valued logics
SMT
theorem prover
Citations: Items that cite this one
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:There is a relatively large number of papers dealing with complexity and proof theory issues of infinitely-valued logics. Nevertheless, little attention has been paid so far to the development of efficient solvers for such logics. In this paper we show how the technology of Satisfiability Modulo Theories (SMT) can be used to build efficient automated theorem provers for relevant infinitely-valued logics, including Lukasiewicz, Gödel and Product logics. Moreover, we define a test suite for those logics, and report on an experimental investigation that evaluates the practical complexity of Lukasiewicz and Gödel logics, and provides empirical evidence of the good performance of SMT technology for automated theorem proving on infinitely-valued logics.
ISSN:0195-623X
2378-2226
DOI:10.1109/ISMVL.2012.63