HERBRAND THEOREMS: THE CLASSICAL AND INTUITIONISTIC CASES

• Authors: Lyaletski Alexander
• Languages of publication: EN

Abstracts

EN

A unified approach is applied for the construction of sequent forms of the famous Herbrand theorem for first-order classical and intuitionistic logics without equality. The forms do not explore skolemization, have wording on deducibility, and as usual, provide a reduction of deducibility in the first-order logics to deducibility in their propositional fragments. They use the original notions of admissibility, compatibility, a Herbrand extension, and a Herbrand universe being constructed from constants, special variables, and functional symbols ccurring in the signature of a formula under investigation. The ideas utilized in the research may be applied for the construction and theoretical investigations of various computer-oriented calculi for efficient logical inference search without skolemization in both classical and intuitionistic logics and provide some new technique for further development of methods for automated reasoning in non-classical logics.

Keywords

EN

AUTOMATED REASONING; CLASSICAL LOGIC; HERBRAND THEOREM; INTUITIONISTIC LOGIC; NON-CLASSICAL LOGICS

Discipline

• LIBRARY_&_INFORMATION_SCIENCE: LIBRARY & INFORMATION SCIENCE

• Publisher: Sciendo
• Journal: Studies in Logic, Grammar and Rhetoric
• Year: 2008
• Issue: 14(27)
• Pages: 101-122
• Document type: ARTICLE

Contributors

author

Lyaletski Alexander

• Alexander Lyaletski, Faculty of Cybernetics, Kyiv National Taras Shevchenko University, Kyiv, Ukraine

Identifiers

CEJSH db identifier

11PLAAAA101412