Herbrand Theorems for Substructural Logics

Autoři: doc. Ing. Petr Cintula, Ph.D. DSc.
Rok vydání: 2013
Typ publikace: Konferenční příspěvek (mezinárodní konf.)
Periodikum: Logic for Programming, Artificial Intelligence, and Reasoning
Projekty: Matematická fuzzy logika v informatice
Bibliografická citace: CINTULA, Petr, METCALFE, G. Herbrand Theorems for Substructural Logics. In: MCMILLAN, K., MIDDELDORP, A., VORONKOV, A., eds. Logic for Programming, Artificial Intelligence, and Reasoning. Berlin: Springer, 2013, S. 584-600. Lecture Notes in Computer Science, 8312. ISBN 978-3-642-45221-5. ISSN 0302-9743
Dostupné z: doi:10.1007/978-3-642-45221-5_39
DOI: 10.1007/978-3-642-45221-5_39
ID: 422069

Abstrakt

Herbrand and Skolemization theorems are obtained for a broad family of first-order substructural logics. These logics typically lack equivalent prenex forms, a deduction theorem, and reductions of semantic consequence to satisfiability. The Herbrand and Skolemization theorems therefore take various forms, applying either to the left or right of the consequence relation, and to restricted classes of formulas.