History

Please fill in your query. A complete syntax description you will find on the General Help page.
Sequent calculus Sk4 for skolemized formulas. (English)
Liet. Mat. Rink. 45, Spec. Iss., 316-320 (2005).
Summary: We consider the formulas of quantified modal logic which contain the logical connectives $\neg$, $\&$, $\vee$, and the negation occurs only in front of atomic formulas. This means that the considered formulas are in normal negation form. We consider two ways of Skolemization: outer and inner (cf. [{\it A. Nonnengart}, Strong Skolemization. Research Report MPI-I-96-2-010, Saarbrücken, Max-Plank-Institute für Informatik (1996)] for the case of classical logic).