Citation: G. Dowek, Automated theorem proving in first-order logic module: On the difference between type theory and set theory, LECT N A I, 1761, 2000, pp. 1-22
Citation: A. Leitsch, Decision procedures and model building or how to improve logical information in automated deduction, LECT N A I, 1761, 2000, pp. 62-79
Citation: D. Cantone et Mn. Asmundo, A further and effective liberalization of the delta-rule in free variable semantic tableaux, LECT N A I, 1761, 2000, pp. 109-125
Citation: D. Cantone et Cg. Zarba, A new fast tableau-based decision procedure for an unquantified fragment of set theory, LECT N A I, 1761, 2000, pp. 126-136
Citation: S. Demri et R. Gore, An O((n center dot log n)(3))-time transformation from Grz into decidable fragments of classical first-order logic, LECT N A I, 1761, 2000, pp. 152-166
Citation: Cp. Wirth, Full first-order sequent and tableau calculi with preservation of solutions and the liberalized delta-rule but without Skolemization, LECT N A I, 1761, 2000, pp. 282-297