Herbrand's Theorem, Skolemization and Proof Systems for First-Order Lukasiewicz Logic

DOI10.1093/logcom/exn059zbMath1188.03014OpenAlexW1966718868MaRDI QIDQ3406683

Matthias Baaz, George Metcalfe

Publication date: 19 February 2010

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/logcom/exn059

zbMATH Keywords

proof theoryMV-algebraŁukasiewicz logichypersequentSkolemizationHerbrand theorem

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) MV-algebras (06D35) Many-valued logic (03B50)

Related Items

Free-variable semantic tableaux for the logic of fuzzy inequalities, Infinite-Valued First-Order Łukasiewicz Logic: Hypersequent Calculi Without Structural Rules and Proof Search for Sentences in the Prenex Form, Comparing Calculi for First-Order Infinite-Valued Łukasiewicz Logic and First-Order Rational Pavelka Logic, Herbrand Theorems and Skolemization for Prenex Fuzzy Logics, The eskolemization of universal quantifiers, Repetition-free and infinitary analytic calculi for first-order rational Pavelka logic, Skolemization and Herbrand theorems for lattice-valued logics, The Skolemization of prenex formulas in intermediate logics, Triangular norm based predicate fuzzy logics, Unnamed Item, Giles's game and the proof theory of Łukasiewicz logic