Title :
Chaining techniques for automated theorem proving in many-valued logics
Author :
Ganzinger, Harald ; Sofronie-Stokkermans, Viorica
Author_Institution :
Max-Planck-Inst. fur Inf., Saarbrucken, Germany
Abstract :
We apply chaining techniques to automated theorem proving in many-valued logics. In particular, we show that superposition specializes to a refined version of the many-valued resolution rules introduced by Baaz and Fermuller, and that ordered chaining can be specialized to a refutationally complete inference system for regular clauses
Keywords :
multivalued logic; theorem proving; automated theorem proving; chaining techniques; inference system; many-valued logics; many-valued resolution rules; superposition; Constraint theory; Encoding; Multivalued logic; Postal services; Terminology;
Conference_Titel :
Multiple-Valued Logic, 2000. (ISMVL 2000) Proceedings. 30th IEEE International Symposium on
Conference_Location :
Portland, OR
Print_ISBN :
0-7695-0692-5
DOI :
10.1109/ISMVL.2000.848641
