Skolemization for Substructural Logics

0448462 - ÚI 2016 RIV DE eng C - Konferenční příspěvek (zahraniční konf.)
Cintula, Petr - Diaconescu, D. - Metcalfe, G.
Skolemization for Substructural Logics.
Logic for Programming, Artificial Intelligence, and Reasoning. Berlin: Springer, 2015 - (Davis, M.; Fehnker, A.; McIver, A.; Voronkov, A.), s. 1-15. Lecture Notes in Computer Science, 9450. ISBN 978-3-662-48898-0. ISSN 0302-9743.
[LPAR-20. International Conference /20./. Suva (JP), 24.11.2015-28.11.2015]
Grant CEP: GA ČR GBP202/12/G061
Institucionální podpora: RVO:67985807
Klíčová slova: substructural logics * first-order logic * Skolemization * witnessed model property
Kód oboru RIV: BA - Obecná matematika

The usual Skolemization procedure, which removes strong quantifiers by introducing new function symbols, is in general unsound for first-order substructural logics defined based on classes of complete residuated lattices. However, it is shown here (following similar ideas of Baaz and Iemho for first-order intermediate logics in [1]) that firstorder substructural logics with a semantics satisfying certain witnessing conditions admit a " Skolemization procedure where a strong quantifier is removed by introducing a finite disjunction or conjunction (as appropriate) of formulas with multiple new function symbols. These logics typically lack equivalent prenex forms. Also, semantic consequence does not in general reduce to satisfiability. The Skolemization theorems presented here therefore take various forms, applying to the left or right of the consequence relation, and to all formulas or only prenex formulas.
Trvalý link: http://hdl.handle.net/11104/0250157