Skolemization and Herbrand Theorems for Lattice-Valued Logics

Cintula, Petr; Diaconescu, Denisa; Metcalfe, George (2019). Skolemization and Herbrand Theorems for Lattice-Valued Logics. Theoretical computer science, 768, pp. 54-75. Elsevier 10.1016/j.tcs.2019.02.007

[img]
Preview
Text
cdm-skolem.pdf - Submitted Version
Available under License Creative Commons: Attribution-Noncommercial-No Derivative Works (CC-BY-NC-ND).

Download (254kB) | Preview
[img] Text
1-s2.0-S0304397519301057-main.pdf - Published Version
Restricted to registered users only
Available under License Publisher holds Copyright.

Download (572kB)

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.

Item Type:

Journal Article (Original Article)

Division/Institute:

08 Faculty of Science > Department of Mathematics and Statistics > Institute of Mathematics

UniBE Contributor:

Diaconescu, Denisa, Metcalfe, George

Subjects:

500 Science > 510 Mathematics

ISSN:

0304-3975

Publisher:

Elsevier

Language:

English

Submitter:

George Metcalfe

Date Deposited:

25 Apr 2019 14:37

Last Modified:

05 Dec 2022 15:27

Publisher DOI:

10.1016/j.tcs.2019.02.007

BORIS DOI:

10.7892/boris.127736

URI:

https://boris.unibe.ch/id/eprint/127736

Actions (login required)

Edit item Edit item
Provide Feedback