Skolemization and Herbrand theorems for lattice-valued logics

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F19%3A00501613" target="_blank" >RIV/67985807:_____/19:00501613 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1016/j.tcs.2019.02.007" target="_blank" >http://dx.doi.org/10.1016/j.tcs.2019.02.007</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1016/j.tcs.2019.02.007" target="_blank" >10.1016/j.tcs.2019.02.007</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Skolemization and Herbrand theorems for lattice-valued logics

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Skolemization and Herbrand theorems for lattice-valued logics

Popis výsledku anglicky

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.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

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í

2019

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 periodika

Theoretical Computer Science

ISSN

0304-3975

e-ISSN

—

Svazek periodika

768

Číslo periodika v rámci svazku

10 May

Stát vydavatele periodika

NL - Nizozemsko

Počet stran výsledku

22

Strana od-do

54-75

Kód UT WoS článku

000466456500003

EID výsledku v databázi Scopus

2-s2.0-85061573241