Abstracts Vol. 9-No 4/ 1999
Next
Previous
Summaries
Abstract: This paper introduces a multi-valued variant of higher-order resolution and proves it correct and complete with respect to a variant of Henkin's general model semantics. This resolution method is parametric in the number of truth values as well as in the particular choice of the set of connectives (given by arbitrary truth tables) and even substitutional quantifiers. In the course of the completeness proof we establish a model existence theorem for this logical system. The work reported in this paper provides a basis for developing higher-order mechanizations for many non-classical logics..
Keywords: higher-order logic, resolution, multi-valued, lambda-calculus
Abstract: This paper reports on an empirical analysis of four modal theorem provers on benchmark suites of randomly generated formulae. The theorem provers tested are the Davis-Putnam-based procedure KSAT, the tableaux-based system KRLS, the sequent-based Logics Workbench, and a translation approach combined with the first-order theorem prover SPASS.
Our benchmark suites are sets of multi-modal formulae in a certain normal form randomly generated according to the scheme of Giunchiglia and Sebastiani [GS 96a, GS96b]. We investigate the quality of the random modal formulae and show that the scheme has some shortcomings, which may lead to mistaken conclusions. We propose improvements to the evaluation method and show that the translation aproach provides a viable alternative to the other approaches..
Keywords: Modal logic, automated theorem proving, performance analysis
Abstract: This paper presents the axiomatization --- without the rule of irreflexivity --- of the modal logic of inequality as well as a method for proving its completeness. This method uses the technics of the frame of subordination..
Keywords:
Journal of Applied Non-Classical Logics
Volume 9- No 4/ 1999
Next
Previous
Summaries