摘要:

We are concerned with the theorem proving in annotated logics. By using annotated polynomials to express knowledge, we develop an inference rule superposition. A proof procedure is thus presented, and an improvement named M- strategy is mainly described. This proof procedure uses single overlaps instead of multiple overlaps, and above all, both the proof procedure and M-strategy are refutationally complete.

ISSN:1166-3081    

DOI:10.1080/11663081.2000.10510993

出版商:Taylor & Francis Group    

年代:2000

数据来源: Taylor

摘要:

This paper follows on previous papers which present and evaluate various decision procedures for modal logics. We consider new test sets and systems that have been recently proposed in the literature. This new experimental analysis confirm previous experimental results in showing that SAT based decision procedures, i.e., the procedures built on top of decision procedures for propositional satisfiability, are more efficient than tableau based decision procedures. They also confirm previous evidence of an easy-hard-easy pattern in the satisfiability curve for modal K. Finally, on these tests, SAT based decision procedures are also more efficient than the recently proposed decision procedures based on translation methods. These results contradict some of the claims presented in previous papers by other authors.

ISSN:1166-3081    

DOI:10.1080/11663081.2000.10510994

出版商:Taylor & Francis Group    

年代:2000

数据来源: Taylor

摘要:

We present a new method for proving theorems in the equational theory of partial maps over toposes introduced in the papers [C'089] and [086], The method is given by a system of rules of formation of proofs. The proofs of f() is defined' and the proofs of correctness ‘φ(f())' formed by application of the rules of the system are such that they contain a computation of the value f(), where f is a partial function valued in natural numbers andis a vector of natural numbers. We show that the system is complete, i.e. if an equation holds in every model then it has a proof formed by application of the rules of the system. The system is equipped with a method of visual presentation of proofs by nested commutative triangles, i.e. commutative triangles which contain in their interiors other commutative triangles which may be also nested. To provide formal foundations for the method of visual presentation of proofs we give a mathematical description of nested commutative triangles in terms of directed graphs and graph homomorphisms. AMS Subject Classification 1995: Primary: 68. Secondary: 18.

ISSN:1166-3081    

DOI:10.1080/11663081.2000.10510995

出版商:Taylor & Francis Group    

年代:2000

数据来源: Taylor

ISSN:1166-3081    

DOI:10.1080/11663081.2000.10510996

出版商:Taylor & Francis Group    

年代:2000

数据来源: Taylor

ISSN:1166-3081    

DOI:10.1080/11663081.2000.10510992

出版商:Taylor & Francis Group    

年代:2000

数据来源: Taylor