Skolemization for Substructural Logics

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F15%3A00448462" target="_blank" >RIV/67985807:_____/15:00448462 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-662-48899-7_1" target="_blank" >http://dx.doi.org/10.1007/978-3-662-48899-7_1</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-662-48899-7_1" target="_blank" >10.1007/978-3-662-48899-7_1</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Skolemization for Substructural Logics

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Skolemization for Substructural Logics

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

BA - Obecná matematika

OECD FORD obor

—

Projekt

<a href="/cs/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Centrum excelence - Institut teoretické informatiky (CE-ITI)</a><br>

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2015

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Logic for Programming, Artificial Intelligence, and Reasoning

ISBN

978-3-662-48898-0

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

15

Strana od-do

1-15

Název nakladatele

Springer

Místo vydání

Berlin

Místo konání akce

Suva

Datum konání akce

24. 11. 2015

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—