Number of the records: 1
Skolemization and Herbrand theorems for lattice-valued logics
- 1.
SYSNO ASEP 0501613 Document Type J - Journal Article R&D Document Type Journal Article Subsidiary J Článek ve WOS Title Skolemization and Herbrand theorems for lattice-valued logics Author(s) Cintula, Petr (UIVT-O) RID, ORCID, SAI
Diaconescu, D. (RO)
Metcalfe, G. (CH)Source Title Theoretical Computer Science. - : Elsevier - ISSN 0304-3975
Roč. 768, 10 May (2019), s. 54-75Number of pages 22 s. Language eng - English Country NL - Netherlands Keywords Skolemization ; Herbrand theorems ; Non-classical logics ; Lattices Subject RIV BA - General Mathematics OECD category Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8) R&D Projects GBP202/12/G061 GA ČR - Czech Science Foundation (CSF) Method of publishing Limited access Institutional support UIVT-O - RVO:67985807 UT WOS 000466456500003 EID SCOPUS 85061573241 DOI 10.1016/j.tcs.2019.02.007 Annotation Skolemization and Herbrand theorems are obtained for first-order logics based on algebras with a complete lattice reduct and operations that are monotone or antitone in each argument. These lattice-valued logics, defined as consequence relations on inequations between formulas, typically lack properties underlying automated reasoning in classical first-order logic such as prenexation, deduction theorems, or reductions from consequence to satisfiability. Skolemization and Herbrand theorems for the logics therefore take various forms, applying to the left or right of consequences, and restricted classes of inequations. In particular, in the presence of certain witnessing conditions, they admit sound “parallel” Skolemization procedures where a strong quantifier is removed by introducing a finite disjunction or conjunction of formulas with new function symbols. A general expansion lemma is also established that reduces consequence in a lattice-valued logic between inequations containing only strong occurrences of quantifiers on the left and weak occurrences on the right to consequence between inequations in the corresponding propositional logic. If propositional consequence is finitary, this lemma yields a Herbrand theorem for the logic. Workplace Institute of Computer Science Contact Tereza Šírová, sirova@cs.cas.cz, Tel.: 266 053 800 Year of Publishing 2020 Electronic address http://dx.doi.org/10.1016/j.tcs.2019.02.007
Number of the records: 1