Premium
A Many‐Sorted Natural Deduction
Author(s) -
Cimatti A.,
Giunchiglia F.,
Weyhrauch R. W.
Publication year - 1998
Publication title -
computational intelligence
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.353
H-Index - 52
eISSN - 1467-8640
pISSN - 0824-7935
DOI - 10.1111/0824-7935.00058
Subject(s) - natural deduction , sequent calculus , extension (predicate logic) , calculus (dental) , computer science , focus (optics) , natural (archaeology) , mathematics , algorithm , artificial intelligence , programming language , mathematical proof , medicine , physics , geometry , dentistry , optics , archaeology , history
The goal of this paper is to motivate and define yet another sorted logic, called SND. All the previous sorted logics that can be found in the Artificial Intelligence literature have been designed to be used in (completely) automated deduction . SND has been designed to be used in interactive theorem proving. Because of this shift of focus, SND has been designed to satisfy three innovative design requirements: it is defined on top of a natural deduction calculus, and in a way to be a definitional extension of such calculus; and it is implemented on top of its implementation. In turn, because of this fact, SND has various innovative technical properties; among them: it allows us to deal with free variables, it has no notion of well‐sortedness and of well‐sortedness being a prerequisite of well‐formedness, its implementation is such that, in the default mode, the system behaves exactly as with the original unsorted calculus.