In this paper we present SND, a natural deduction system extended with sorts, and show that it is particularly suited for interactive theorem proving. SND allows for a natural representation of informal arguments. Its main characteristics are the eliminability of sorts by theorem proving within SND itself, and a natural treatment of restricted free variables. SND is the logic implemented in the FOL system
A Many Sorted Natural Deduction
Cimatti, Alessandro;Giunchiglia, Fausto;
1998-01-01
Abstract
In this paper we present SND, a natural deduction system extended with sorts, and show that it is particularly suited for interactive theorem proving. SND allows for a natural representation of informal arguments. Its main characteristics are the eliminability of sorts by theorem proving within SND itself, and a natural treatment of restricted free variables. SND is the logic implemented in the FOL systemFile in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
