Automated deduction in classical and non-classical logics. Selected papers (Q1967066)

The articles of this volume will be reviewed individually. Indexed articles: \textit{Dowek, Gilles}, Automated theorem proving in first-order logic modulo: On the difference between type theory and set theory, 1-22 [Zbl 0960.03008] \textit{Fitting, Melvin}, Higher-order modal logic -- a sketch, 23-38 [Zbl 0955.03030] \textit{Kapur, Deepak; Sivakumar, G.}, Proving associative-commutative termination using RPO-compatible orderings, 39-61 [Zbl 0963.68089] \textit{Leitsch, Alexander}, Decision procedures and model building or how to improve logical information in automated deduction, 62-79 [Zbl 0966.03011] \textit{Plaisted, David A.; Zhu, Yunshan}, Replacement rules with definition detection, 80-94 [Zbl 0963.68194] \textit{Boy de la Tour, Thierry}, On the complexity of finite sorted algebras, 95-108 [Zbl 0964.08007] \textit{Cantone, Domenico; Nicolosi Asmundo, Marianna}, A further and effective liberalization of the \(\delta\)-rule in free variable semantic tableaux, 109-125 [Zbl 0955.03014] \textit{Cantone, Domenico; Zarba, Calogero G.}, A new fast tableau-based decision procedure for an unquantified fragment of set theory, 126-136 [Zbl 0955.03015] \textit{Dahn, Ingo}, Interpretation of a Mizar-like logic in first order logic, 137-151 [Zbl 0960.03007] \textit{Demri, Stéphane; Goré, Rajeev}, An \({\mathcal O}((n\log n)^3)\)-time transformation from Grz into decidable fragments of classical first-order logic, 152-166 [Zbl 0956.03026] \textit{Fermüller, Christian G.}, Implicational completeness of signed resolution, 167-174 [Zbl 0962.03008] \textit{Formisano, Andrea; Omodeo, Eugenio}, An equational re-engineering of set theories, 175-190 [Zbl 0955.03016] \textit{Hustadt, Ullrich; Schmidt, Renate A.}, Issues of decidability for description logics in the framework of resolution, 191-205 [Zbl 0955.03018] \textit{Pichler, Reinhard}, Extending decidable clause classes via constraints, 206-220 [Zbl 0955.03020] \textit{Pichler, Reinhard}, Completeness and redundancy in constrained clause logic, 221-235 [Zbl 0955.03019] \textit{Pliuškevičienė, Aida}, Effective properties of some first order intuitionistic modal logics, 236-250 [Zbl 0963.03034] \textit{Roşu, Grigore; Goguen, Joseph}, Hidden congruent deduction, 251-266 [Zbl 0964.68083] \textit{Sofronie-Stokkermans, Viorica}, Resolution-based theorem proving for \(\text{SH}_n\)-logics, 267-281 [Zbl 0956.03009] \textit{Wirth, Claus-Peter}, Full first-order sequent and tableau calculi with preservation of solutions and the liberalized \(\delta\)-rule but without Skolemization, 282-297 [Zbl 0955.03021]