ISSN:1166-3081    

DOI:10.1080/11663081.1999.10510979

出版商:Taylor & Francis Group    

年代:1999

数据来源: Taylor

摘要:

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.

ISSN:1166-3081    

DOI:10.1080/11663081.1999.10510980

出版商:Taylor & Francis Group    

年代:1999

数据来源: Taylor

摘要:

This paper reports on an empirical performance analysis of four modal theorem provers on benchmark suites of randomly generated formulae. The theorem provers tested are the Davis-Putnam-based procedureKSAT, the tableaux-based system KRZIS, the sequent-based Logics Workbench, and a translation approach combined with the first-order theorem prover SPASS.

ISSN:1166-3081    

DOI:10.1080/11663081.1999.10510981

出版商:Taylor & Francis Group    

年代:1999

数据来源: Taylor

摘要:

This paper presents the axioinatization—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.

ISSN:1166-3081    

DOI:10.1080/11663081.1999.10510982

出版商:Taylor & Francis Group    

年代:1999

数据来源: Taylor

ISSN:1166-3081    

DOI:10.1080/11663081.1999.10510983

出版商:Taylor & Francis Group    

年代:1999

数据来源: Taylor

ISSN:1166-3081    

DOI:10.1080/11663081.1999.10510984

出版商:Taylor & Francis Group    

年代:1999

数据来源: Taylor

ISSN:1166-3081    

DOI:10.1080/11663081.1999.10510978

出版商:Taylor & Francis Group    

年代:1999

数据来源: Taylor