排序方式: 共有99条查询结果,搜索用时 125 毫秒
1.
Dmitrij Skvortsov 《Studia Logica》1997,59(3):387-396
An example of finite tree Mo is presented such that its predicate logic (i.e. the intermediate predicate logic characterized by the class of all predicate Kripke frames based on Mo) is not finitely axiomatizable. Hence it is shown that the predicate analogue of de Jongh - McKay - Hosoi's theorem on the finite axiomatizability of every finite intermediate propositional logic is not true. 相似文献
2.
Game logic and its applications I 总被引:3,自引:0,他引:3
This paper provides a logic framework for investigations of game theoretical problems. We adopt an infinitary extension of classical predicate logic as the base logic of the framework. The reason for an infinitary extension is to express the common knowledge concept explicitly. Depending upon the choice of axioms on the knowledge operators, there is a hierarchy of logics. The limit case is an infinitary predicate extension of modal propositional logic KD4, and is of special interest in applications. In Part I, we develop the basic framework, and show some applications: an epistemic axiomatization of Nash equilibrium and formal undecidability on the playability of a game. To show the formal undecidability, we use a term existence theorem, which will be proved in Part II.The authors thank Hiroakira Ono for helpful discussions and encouragements from the early stage of this research project, and Philippe Mongin, Mitio Takano and a referee of this journal for comments on earlier versions of this paper. The first and second authors are partially supported, respectively, by Tokyo Center of Economic Research and Grant-in-Aids for Scientific Research 04640215, Ministry of Education, Science and Culture.Presented by H. Ono 相似文献
3.
Alessandro Avellone Camillo Fiorentini Paolo Mantovani Pierangelo Miglioli 《Studia Logica》1996,57(2-3):373-408
We extend to the predicate frame a previous characterization of the maximal intermediate propositional constructive logics. This provides a technique to get maximal intermediate predicate constructive logics starting from suitable sets of classically valid predicate formulae we call maximal nonstandard predicate constructive logics. As an example of this technique, we exhibit two maximal intermediate predicate constructive logics, yet leaving open the problem of stating whether the two logics are distinct. Further properties of these logics will be also investigated.Presented by H. Ono 相似文献
4.
We introduce non-associative linear logic, which may be seen as the classical version of the non-associative Lambek calculus. We define its sequent calculus, its theory of proof-nets, for which we give a correctness criterion and a sequentialization theorem, and we show proof search in it is polynomial. 相似文献
5.
6.
The paper provides a uniform Gentzen-style proof-theoretic framework for various subsystems of classical predicate logic. In particular, predicate logics obtained by adopting van Behthem's modal perspective on first-order logic are considered. The Gentzen systems for these logics augment Belnap's display logic by introduction rules for the existential and the universal quantifier. These rules for x and x are analogous to the display introduction rules for the modal operators and and do not themselves allow the Barcan formula or its converse to be derived. En route from the minimal modal predicate logic to full first-order logic, axiomatic extensions are captured by purely structural sequent rules. 相似文献
7.
A general class of labeled sequent calculi is investigated, and necessary and sufficient conditions are given for when such a calculus is sound and complete for a finite-valued logic if the labels are interpreted as sets of truth values (sets-as-signs). Furthermore, it is shown that any finite-valued logic can be given an axiomatization by such a labeled calculus using arbitrary "systems of signs," i.e., of sets of truth values, as labels. The number of labels needed is logarithmic in the number of truth values, and it is shown that this bound is tight. 相似文献
8.
A tableau is a refutation-based decision procedure for a related logic, and is among the most popular proof procedures for modal logics. In this paper, we present a labelled tableau calculus for a temporalised belief logic called TML+, which is obtained by adding a linear-time temporal logic onto a belief logic by the temporalisation method of Finger and Gabbay. We first establish the soundness and the completeness of the labelled tableau calculus based on the soundness and completeness results of its constituent logics. We then sketch a resolution-type proof procedure that complements the tableau calculus and also propose a model checking algorithm for TML+ based on the recent results for model checking procedures for temporalised logics. TML+ is suitable for formalising trust and agent beliefs and reasoning about their evolution for agent-based systems. Based on the logic TML+, the proposed labelled tableau calculus could be used for analysis, design and verification of agent-based systems operating in dynamic environments. 相似文献
9.
Barry Hartley Slater 《Synthese》2008,163(2):187-198
Prawitz proved a theorem, formalising ‘harmony’ in Natural Deduction systems, which showed that, corresponding to any deduction
there is one to the same effect but in which no formula occurrence is both the consequence of an application of an introduction
rule and major premise of an application of the related elimination rule. As Gentzen ordered the rules, certain rules in Classical
Logic had to be excepted, but if we see the appropriate rules instead as rules for Contradiction, then we can extend the theorem to the classical case. Properly arranged there is a thoroughgoing ‘harmony’, in the classical
rules. Indeed, as we shall see, they are, all together, far more ‘harmonious’ in the general sense than has been commonly
observed. As this paper will show, the appearance of disharmony has only arisen because of the illogical way in which natural
deduction rules for Classical Logic have been presented. 相似文献
10.
In this paper, we show the weak normalization (WN) of the simply-typedse-calculus with open terms where abstractions are decoratedwith types, and metavariables, de Bruijn indices and updatingoperators are decorated with environments. We show a proof ofWN using the e-calculus, a calculus isomorphic to . This proof is strongly influenced by Goubault-Larrecq'sproof of WN for the -calculus but with subtle differences whichshow that the two styles require different attention. Furthermore,we give a new calculus 'e which works like se but which iscloser to than e. For both e and 'e we prove WN for typedsemi-open terms (i.e. those which allow term variables but nosubstitution variables), unlike the result of Goubault-Larrecqwhich covered all open terms. 相似文献