Le tableau de Nicolas Poussin, Paysage avec un homme tué par un serpent (ou Les effets de la terreur), demeure énigmatique pour toute une critique qui oscille entre deux pôles : soit le tableau est mythologique, mais on ne sait pas à quelle histoire il renvoie (l’hypothèse de Cadmus n’étant guère soutenable) ; soit le tableau ne représente que les effets de la terreur, sans renvoyer à aucune histoire. La thèse défendue dans cet article est la (...) suivante : tout en représentant les effets de la terreur, le tableau renvoie à une histoire – non celle de Cadmus, mais celle de Narcisse, cet homme qui meurt près de la source qui le captive, prisonnier de l’amour vain qu’il se porte à lui-même. On se propose d’étayer cette thèse par la découverte de remarquables liens entre Narcisse et Python, non seulement à partir de l’œuvre poétique d’Ovide, mais encore à partir de l’œuvre picturale de Poussin. (shrink)

Le Paysage avec un homme tué par un serpent, peint par Nicolas Poussin en 1648, a donné lieu, depuis celles de Félibien, Fénelon ou Diderot, à de multiples lectures, suggérant telle source poétique ou telle gravure pour rendre compte de l’identité du personnage mort ou de celle du serpent, sans qu’aucune de ces hypothèses paraisse décisive. Celle que propose Hélène Bouchilloux désigne Narcisse pour le personnage mort et Python pour le serpent : Poussin aurait mis en scène la « destitution (...) » de l’amour stérile en même temps que celle de l’idée erronée de la peinture incarnée par le Caravage. Cette hypothèse séduisante présente toutefois des difficultés méthodologiques, tant dans l’interprétation du texte d’Ovide que dans l’approche comparative de plusieurs toiles de Poussin, n’évitant pas le risque d’une surinterprétation. (shrink)

Le syndrome de Kierkegaard est un essai libre de Jean- Luc Berlet, consacré à l'un de ses penseurs de prédilection, le Danois Seren Kierkegaard (1813-1855). Ce syndrome dont il est question, tel que défini par l'auteur, pourrait être conçu comme la tension qui résulte de l'impossible choix entre l'amour de la femme et l'amour de Dieu. Kierkegaard renonça en effet à l'amour charnel de la femme au profit d'une vie ascétique consacrée à I écriture et à la réflexion sur l'Amour. (...) A plus grande échelle ce syndrome pourrait être compris comme l'abandon du temporel au profit d'un idéal spirituel Et les regrets qui en découlent. En effet, comme nombre de contemporains opérant ce type de choix, Kierkegaard connut bien des tourments. Ces affres permirent néanmoins à Kierkegaard de développer une conception de l'Amour et du Divin d'une grande originalité qu'il est bon de redécouvrir dans notre époque marquée par le consumérisme sentimental. Tout au long des quatorze chapitres qui jalonnent cet ouvrage, Jean-Luc Berlet retrace le parcours littéraire de ce philosophe danois considéré par beaucoup comme le père de l'existentialisme, brossant ici un tableau complet de son énigmatique personnalité. En outre, chaque chapitre est accompagné d'un code QR, donnant chacun actes à une vidéo en ligne où Jean - Luc Berlet approfondit son développement et fournit des clefs de lecture pour une meilleure compréhension de l'oeuvre de Kierkegaard. (shrink)

Sur la couverture, la reproduction d’un énigmatique tableau de Borduas, chef de file du Refus global des années 40: Le condor embouteillé, symbolise la rupture radicale qui s’annonce dans l’histoire culturelle et sociale du Québec. Le condor philosophique, au vol inverse de celui de la chouette, sort enfin au grand jour de sa captivité théologique.

This paper contributes to the principled construction of tableau-based decision procedures for hybrid logic with global, difference, and converse modalities. We also consider reflexive and transitive relations. For converse-free formulas we present a terminating control that does not rely on the usual chain-based blocking scheme. Our tableau systems are based on a new model existence theorem.

Since 1993, when Hudelmaier developed an O(n log n)-space decision procedure for propositional Intuitionistic Logic, a lot of work has been done to improve the efficiency of the related proof-search algorithms. In this paper a tableau calculus using the signs T, F and Fc with a new set of rules to treat signed formulas of the kind T((A → B) → C) is provided. The main feature of the calculus is the reduction of both the non-determinism in proof-search and (...) the width of proofs with respect to Hudelmaier's one. These improvements have a significant influence on the performances of the implementation. (shrink)

ABSTRACT In this paper we define two logics, KLn and BLn, and present tableau-based decision procedures for both. KLn is a temporal logic of knowledge. Thus, in addition to the usual connectives of linear discrete temporal logic, it contains a set of unary modal connectives for representing the knowledge possessed by agents. The logic BLn is somewhat similar; it is a temporal logic that contains connectives for representing the beliefs of agents. In addition to a complete formal definition of (...) the two logics and their decision procedures, the paper includes a brief review of their applications in AI and mainstream computer science, correctness proofs for the decision procedures, a number of worked examples illustrating the decision procedures, and some pointers to further work. (shrink)

In this paper a first-order version of hybrid logic is presented. The language is obtained by adding nominals, satisfaction operators and the down-arrow binder to classical first-order modal logic. The satisfaction operators are applied to both formulas and terms. Moreover adding the universal modality is discussed. This first-order hybrid language is interpreted over varying domains and a sound and complete, fully internalized tableau system for this logic is given.

Labelled tableau systems are developed for subintuitionistic logics \, \ and \. These subintuitionistic logics are embedded into corresponding normal modal logics. Hintikka’s model systems are applied to prove the completeness of labelled tableau systems. The finite model property, decidability and disjunction property are obtained by labelled tableau method.

Automated theorem proving amounts to solving search problems in usually tremendous search spaces. A lot of research therefore focuses on search space reductions. Our approach reduces the search space which arises when using so-called connection tableau calculi for first-order automated theorem proving. It uses disjunctive constraints over first-order equations to compress certain parts of this search space. We present the basics of our constrained-connection-tableau calculi, a constraint extension of connection tableau calculi, and deal with the efficient handling (...) of constraints during the search process. The new techniques are integrated into the automated connection tableau prover Setheo. (shrink)

Automated theorem proving amounts to solving search problems in usually tremendous search spaces. A lot of research therefore focuses on search space reductions. Our approach reduces the search space which arises when using so-called connection tableau calculi for first-order automated theorem proving. It uses disjunctive constraints over first-order equations to compress certain parts of this search space. We present the basics of our constrained-connection-tableau calculi, a constraint extension of connection tableau calculi, and deal with the efficient handling (...) of constraints during the search process. The new techniques are integrated into the automated connection tableau prover Setheo. (shrink)

We introduce a family of tableau calculi for deontic action logics based on finite boolean algebras, these logics provide deontic operators which are applied to a finite number of actions ; furthermore, in these formalisms, actions can be combined by means of boolean operators, this provides an expressive algebra of actions. We define a tableau calculus for the basic logic and then we extend this calculus to cope with extant variations of this formalism; we prove the soundness and (...) completeness of these proof systems. In addition, we investigate the computational complexity of the satisfiability problem for DAL and its extensions; we show this problem is NP-complete when the number of actions considered is fixed, and it is \-Hard when the number of actions is taken as an extra parameter. The tableau systems introduced here can be implemented in PSPACE, this seems reasonable taking into consideration the computational complexity of the logics. (shrink)

Peirce’s triadic logic has been under discussion since its discovery in the 1960s by Fisch and Turquette. The experiments with matrices of three-valued logic are recorded in a few pages of unpublished manuscripts dated 1909, a decade before similar systems have been developed by logicians. The purposes of Peirce’s work on such logic, as well as semantical aspects of his system, are disputable. In the most extensive work about it, Turquette suggested that the matrices are related in dual pairs of (...) axiomatic Hilbert-style systems. In this paper, we present a simple tableau proof for a fragment of Peirce three-valued logic, called P3, based on similar approaches in many-valued literature. We demonstrated that this proof is sound and complete. Besides that, taking the false as the only undesignated value and adding non-classical negations to the calculus, we can explore paraconsistent and paracompleteness theories into P3. Keywords: Charles S. Peirce, many-valued logics, theory of proof, tableau method. (shrink)

Le Tableau naturel des rapports qui existent entre Dieu, l'homme et l'univers est un ouvrage fondamental pour ceux qui cherchent à comprendre les mystères de la Création. Pour Louis-Claude de Saint-Martin, l'homme porte en lui-même la clé de tous les mystères. Se connaître soi-même est donc la condition primordiale pour accéder à la Connaissance. Les textes sacrés nous enseignent que l'histoire de l'humanité est liée à un drame en trois actes. Le premier est celui de l'âge d'or ; le (...) deuxième celui d'une chute douloureuse dans la matière ; le troisième, qui reste à venir, sera marqué par une rédemption, une réintégration dans le Divin. L'auteur de ce livre s'efforce de percer le sens ésotérique de ces trois étapes. Il montre aussi que l'impasse dans laquelle se trouve l'homme résulte de la confusion qui règne dans ses pensées. S'il nourrissait sa volonté à la chaleur de l'Amour divin, il accéderait à la régénération d'une manière naturelle, et l'humanité trouverait la Connaissance menant à la Paix Profonde. (shrink)

In Symbolic Logic (1932), C. I. Lewis developed five modal systems S1 − S5. S4 and S5 are so-called normal modal systems. Since Lewis and Langford’s pioneering work many other systems of this kind have been investigated, among them the 32 systems that can be generated by the five axioms T, D, B, 4 and 5. Lewis also discusses how his systems can be augmented by propositional quantifiers and how these augmented logics allow us to express some interesting ideas that (...) cannot be expressed in the corresponding quantifier-free logics. In this paper, I will develop 64 normal modal semantic tableau systems that can be extended by propositional quantifiers yielding 64 extended systems. All in all, we will investigate 128 different systems. I will show how these systems can be used to prove some interesting theorems and I will discuss Lewis’s so-called existence postulate and some of its consequences. Finally, I will prove that all normal modal systems are sound and complete and that all systems (including the extended systems) are sound with respect to their semantics. It is left as an open question whether or not the extended systems are complete. (shrink)

Most of this work is devoted to presenting aspects of proof theory that have developed out of Gentzen's work. Thus the them is "cut elimination" and transfinite induction over constructive ordinals. Smullyan's tableau systems will be used for the formalisms and some of the basic logical results as presented in Smullyan [1] will be assumed to be known (essentially only the classical completeness and consistency proofs for propositional and first order logic).

The final moments of King Vidor's melodrama, Stella Dallas is famous as a tableau of exquisite pathos and feeling. This paper examines Stanley Cavell's reading of Vidor's tableau of an unknown woman in relation to Linda Williams's earlier feminist reading, it examines Cavell's dispute with Williams and seeks to offer a different reading of the film that takes the contemporary art historical discourse about tableau as its guide, and comes to the conclusion that Vidor's tableau anticipates (...) the 'return to painting' that marks Jeff Wall's famous photographic lightbox Picture for Women. Vidor's tableau is itself a lightbox that articulates the tension in American culture and life between the propriety of social order and the impropriety of modern social mobility. (shrink)

Even though it is not very often admitted, partial functions do play a significant role in many practical applications of deduction systems. Kleene has already given a semantic account of partial functions using a three-valued logic decades ago, but there has not been a satisfactory mechanization. Recent years have seen a thorough investigation of the framework of many-valued truth-functional logics. However, strong Kleene logic, where quantification is restricted and therefore not truthfunctional, does not fit the framework directly. We solve this (...) problem by applying recent methods from sorted logics. This paper presents a tableau calculus that combines the proper treatment of partial functions with the efficiency of sorted calculi. (shrink)

In [6] proof tableau formulations were given of the implication/negation fragments of the important zero-order relevant logics E and R and the semirelevant logic RM . The main purpose of this paper then, is to extend results by giving proof tableau formulations of the distribution-free fragments of E, R and RM and of their first order extensions EQ, RQ and RMQ. Where X is one of these logics, we shall follow [13] in calling its distribution-free fragment OX – (...) the ‘O’ standing for ‘ortho’ which is meant to signify the kinship of these logics to quantum logics or ortho-logics as they now tend to be known. Hence in what follows we shall refer to the logics OX simply as relevant ortho-logics. (shrink)

We present a sound and complete tableau calculus for the class of regular grammar logics. Our tableau rules use a special feature called automaton-labelled formulae, which are similar to formulae of automaton propositional dynamic logic. Our calculus is cut-free and has the analytic superformula property so it gives a decision procedure. We show that the known EXPTIME upper bound for regular grammar logics can be obtained using our tableau calculus. We also give an effective Craig interpolation lemma (...) for regular grammar logics using our calculus. (shrink)

We give complete sequent-like tableau systems for the modal logics KB, KDB, K5, and KD5. Analytic cut rules are used to obtain the completeness. Our systems have the analytic superformula property and can thus give a decision procedure. Using the systems, we prove the Craig interpolation lemma for the mentioned logics.

The goal of the article is twofold. The first one is to provide logics based on positional semantics which will be suitable for the analysis of epistemic modalities such as ‘agent... knows/beliefs that...’. The second one is to define tableau systemsfor such logics. Firstly, we present the minimal positional logic MR. Then, we change the notion of formulas and semantics in order to consider iterations of the operator of realization and “free” classical formulas. After that, we move on to (...) weaker logics in order to avoid the well known problem of logical omniscience. At the same time, we keep the positional counterparts of modal axioms, and. For all of the considered logics we present sound and complete tableau systems. (shrink)

The book aims to formalise tableau methods for the logics of propositions and names. The methods described are based on Set Theory. The tableau rule was reduced to an ordered n-tuple of sets of expressions where the first element is a set of premises, and the following elements are its supersets.

Dynamic First Order Logic results from interpreting quantification over a variable v as change of valuation over the v position, conjunction as sequential composition, disjunction as non-deterministic choice, and negation as test for continuation. We present a tableau style calculus for DFOL with explicit binding, prove its soundness and completeness, and point out its relevance for programming with DFOL, for automated program analysis including loop invariant detection, and for semantics of natural language. We also extend this to an infinitary (...) calculus for DFOL with iteration and connect up with other work in dynamic logic. (shrink)

We develop a conceptually clear, intuitive, and feasible decision procedure for testing satisfiability in the full multi\-agent epistemic logic \CMAELCD\ with operators for common and distributed knowledge for all coalitions of agents mentioned in the language. To that end, we introduce Hintikka structures for \CMAELCD\ and prove that satisfiability in such structures is equivalent to satisfiability in standard models. Using that result, we design an incremental tableau-building procedure that eventually constructs a satisfying Hintikka structure for every satisfiable input set (...) of formulae of \CMAELCD\ and closes for every unsatisfiable input set of formulae. (shrink)

Grammar logics were introduced by Fariñas del Cerro and Penttonen in 1988 and have been widely studied. In this paper we consider regular grammar logics with converse ( REG c logics) and present sound and complete tableau calculi for the general satisfiability problem of REG c logics and the problem of checking consistency of an ABox w.r.t. a TBox in a REG c logic. Using our calculi we develop ExpTime (optimal) tableau decision procedures for the mentioned problems, to (...) which various optimization techniques can be applied. We also prove a new result that the data complexity of the instance checking problem in REG c logics is coNP-complete. (shrink)

In this paper, we provide non-clausal tableau calculi for the maximum satisfiability problem and its variants. We discuss both basic calculi to characterize the problem and their modifications to reduce the proof size.

The aim of this paper is to construct a tableau decision algorithm for the modal description logic K ALC with constant domains. More precisely, we present a tableau procedure that is capable of deciding, given an ALC-formula with extra modal operators (which are applied only to concepts and TBox axioms, but not to roles), whether is satisfiable in a model with constant domains and arbitrary accessibility relations. Tableau-based algorithms have been shown to be practical even for logics (...) of rather high complexity. This gives us grounds to believe that, although the satisfiability problem for K ALC is known to be NEXPTIME-complete, by providing a tableau decision algorithm we demonstrate that highly expressive description logics with modal operators have a chance to be implementable. The paper gives a solution to an open problem of Baader and Laux [5]. (shrink)

In order to modelize the reasoning of intelligent agents represented by a poset T, H. Rasiowa introduced logic systems called “Approximation Logics”. In these systems a set of constants constitutes a fundamental tool. In this paper, we consider logic systems called L'T without this kind of constants but limited to the case where T is a finite poset. We study the tableau method for this system and we prove its completeness for a class of formulas with respect to an (...) algebraic semantics. (shrink)

Monoidal triangular norm logic MTL is the logic of left-continuous triangular norms. In the paper we present a relational formalization of the logic MTL and then we introduce relational dual tableau that can be used for verification of validity of MTL-formulas. We prove soundness and completeness of the system.

This paper contains the full code of a prototype implementation in Haskell [5], in ‘literate programming’ style [6], of the tableau-based calculus and proof procedure for hybrid logic presented in [4].

At the beginning of Derrida's ‘Before the Law’, a reading of Kafka's story with that title, is an epigraph from Montaigne's Essays: ‘… science does likewise (and even our law, it is said, has legitimate fictions on which it bases the truth of its justice)…’. Derrida again refers to this quotation in ‘Force of Law’, asking what a ‘legitimate fiction’ might be and what it would mean to establish the basis for the truth of justice. With reference to these writings (...) on the status of narrative and the law, as well as to other texts by Derrida, this paper examines the story of the judge-penitent in Camus' The Fall and, in particular, this ironic reading of the aporetic experience of standing ‘before the law’. What does the narrative, The Fall, entail? Camus writes that the man who speaks in this text is involved in a ‘calculated confession’. How are the borders between truth and fiction, justice and the law, negotiated in this reckoning ‘before the law’? (shrink)

Recent years have been blessed with an abundance of logical systems, arising from a multitude of applications. A logic can be characterised in many different ways. Traditionally, a logic is presented via the following three components: 1. an intuitive non-formal motivation, perhaps tie it in to some application area 2. a semantical interpretation 3. a proof theoretical formulation. There are several types of proof theoretical methodologies, Hilbert style, Gentzen style, goal directed style, labelled deductive system style, and so on. The (...) tableau methodology, invented in the 1950s by Beth and Hintikka and later per fected by Smullyan and Fitting, is today one of the most popular, since it appears to bring together the proof-theoretical and the semantical approaches to the pre of a logical system and is also very intuitive. In many universities it is sentation the style first taught to students. Recently interest in tableaux has become more widespread and a community crystallised around the subject. An annual tableaux conference is being held and proceedings are published. The present volume is a Handbook a/Tableaux pre senting to the community a wide coverage of tableaux systems for a variety of logics. It is written by active members of the community and brings the reader up to frontline research. It will be of interest to any formal logician from any area. (shrink)

We consider fragments of the relational logic RL(1) obtained by posing various constraints on the relational terms involving the operator of composition of relations. These fragments allow to express several non classical logics including modal and description logics. We show how relational dual tableaux can be employed to provide decision procedures for each of them.

We present a dual tableau system, RLK, which is itself a deterministic decision procedure verifying validity of K-formulas. The system is constructed in the framework of the original methodology of relational proof systems, determined only by axioms and inference rules, without any external techniques. Furthermore, we describe an implementation of the system in Prolog, and we show some of its advantages.

Logic has its roots in the study of valid argument, but while traditional logicians worked with natural language directly, modern approaches first translate natural arguments into an artificial language. The reason for this step is that some artificial languages now have very well developed inferential systems. There is no doubt that this is a great advantage in general, but for the study of natural reasoning it is a drawback that the original linguistic forms get lost in translation. An alternative approach (...) would be to develop a general theory of the natural logic behind human reasoning and human information processing by studying formal logics that operate directly on linguistic representations. That this is possible we will try to make plausible in this paper. It will turn out that one level of representation, that of Logical Form, can meaningfully be identified with the language of an existing and well-understood logic, a restricted form of the theory of types. It is not difficult to devise inference systems for this language, and it is thus possible to study reasoning systems that are based directly on language. (shrink)

By introducing and extending description logic (DLs) and growing up their application in knowledge representation and especially in OWLs and semantic web scope, many shortcomings and bugs were identified that weren’t resolvable in classical DLs and so logicians and computer scientists intended to non-classical and non-monotonic reasoning tools. In this paper, I discuses about abduction problem solvers, and by introducing A-Box abduction in description logics (DLs), such as ALC, discuss about decidability and complexity in different introduced algorithms, and report shortly (...) our team’s advantages in developing and implementation of ΑBox abduction in DLs. (shrink)