1,720,995 research outputs found
ARQNL 2018 accompanying code for "A Simple Semi-automated Proof Assistant for First-order Modal Logics"
No full text<p>The file contains the prototype described in the paper.</p>
Cut elimination in inductive proofs of weakly quantified theorems
Full text linkIn dieser Arbeit wird erst der Gentzensche Beweis der Konsistenz der Peano- arithmetik vorgestellt, dann wird die Methode auf eine Klasse induktiver Be- weise erweitert. Da die Schnittregel in der Peanoarithmetik nicht redundant ist, ist Schnittelimination nur für Teilklassen möglich; hier wird die Teilklasse aller induktiven Beweise von Sätzen ohne starke Quantoren untersucht. Es wird gezeigt, dass bei dieser Klasse alle essentiellen Schnitte eliminiert werden können.After presenting Gentzen's cut elimination theorem and the proof of the consistency of Peano arithmetic, we extend the cut elimination procedure to a certain class of inductive proofs. Cut elimination is possible only on subclasses of all inductive proofs. We will investigate the subclass of inductive proofs of theorems without strong quantifiers.We will show that all inductions can be removed following Gentzen's proof of the consistency of Peano arithmetic and therefore, that essential cuts are redundant
Towards Deciding Second-order Unification Problems Using Regular Tree Automata
Full text linkInternational audienceThe second-order unification problem is undecidable [5]. While unification procedures, like Huet's pre-unification, terminate with success on unifiable problems, they might not terminate on non-unifiable ones. There are several decidability results for unification problems with infinitely-many pre-unifiers, such as for monadic second-order problems [3]. These results are based on the regular structure of the solutions of these problems and by computing minimal unifiers. Beyond the importance of the knowledge that searching for unifiers of decidable problems always terminates, one can also use this information in order to optimize unification algorithms, such as in the case for pattern unification [10]. Nevertheless, being able to prove that the unification problem of a certain class of unification constraints is decidable is far from easy. Some results were obtained for certain syntactic restrictions on the problems (see Levy [8] for some results and references) or on the unifiers (see Schmidt-Schauß [11], Schmidt-Schauß and Schulz [12, 13] and Je˙ z [7] for some results). Infinitary unification problems, like the ones we are considering, might suggest that known tools for dealing with the infinite might be useful. One such tool is the regular tree automaton. The drawback of using regular automata for unification is, of course, their inability to deal with variables. In this paper we try to overcome this obstacle and describe an ongoing work about using regular tree automata [1] in order to decide more general second-order unification problems. The second-order unification problems we will consider are of the form λz n .x 0 t. = λz n .C(x 0 s) where C is a non-empty context [2] and x 0 does not occur in t or s. We will call such problems cyclic problems. An important result in second-order unification was obtained by Ganzinger et al. [4] and stated that second-order unification is undecidable already when there is only one second-order variable occurring twice. The unification problem they used for proving the undecidability result was an instance of the following cyclic problem. Note that we chose to use in the definition only unary second-order variables but that this restriction should not be essential. x 0 (w 1 , g(y 1 , a)) = g(y 2 , x 0 (w 2 , a)) (1) Our decidability result is obtained by posing one further restriction over cyclic problems which is based on the existence and location of variables other than the cyclic one. A sufficient condition for the decidability of second-order unification problems was given by Levy [8]. This condition states that if we can never encounter, when applying Huet's pre-unification procedure [6] to a problem, a cyclic equation, then the procedure terminates. It follows from this result that deciding second-order unification problems depends on the ability to decide cyclic problems. The rules of Huet's procedure (PUA) are given in Fig. 1. Imitation partial bindings and projection partial bindings are defined in [14] and are denoted, respectively, by PB(f, α) and PB(i, α) where α is a type, Σ a signature f ∈ Σ and i > 0
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
Variations on the Author
Full text link“Variations on the Author” discusses two of Eduardo Coutinho’s recent films (Um Dia na Vida, from 2010, and Últimas Conversas, posthumously released in 2015) and their contribution to the general question of documentary authorship. The director’s filmography is characterized by a consistent yet self-effacing form of authorial self-inscription: Coutinho often features as an interviewer that rather than express opinions propels discourses; an interviewer that is good at listening. This mode of self-inscription characterizes him as an author who is not expressive but who is nonetheless markedly present on the screen. In Um Dia na Vida, however, Coutinho is completely absent form the image, while Últimas Conversas, on the contrary, includes a confessional prologue that moves the director from the margins to the center of his films. This article examines the ways in which these works stand out in the filmography of a director who offers new insights into the notion of cinematic authorship
Appropriate Similarity Measures for Author Cocitation Analysis
Full text linkWe provide a number of new insights into the methodological discussion about author cocitation analysis. We first argue that the use of the Pearson correlation for measuring the similarity between authors’ cocitation profiles is not very satisfactory. We then discuss what kind of similarity measures may be used as an alternative to the Pearson correlation. We consider three similarity measures in particular. One is the well-known cosine. The other two similarity measures have not been used before in the bibliometric literature. Finally, we show by means of an example that our findings have a high practical relevance.information science;Pearson correlation;cosine;similarity measure;author cocitation analysis
Certification of labeled proofs for modal logics with geometric frame conditions
No full textSeveral proof formalisms have been used, and in some cases even introduced, in order to define proof systems for modal logic. Our work falls within a more general project of establishing a common specification language for checking proofs given in a wide range of deductive formalisms. In this paper, we consider the case of labeled proof systems for modal logics, i.e., in particular, Negri's labeled se-quent calculi, Fitting's prefixed tableaux and free-variable prefixed tableaux, and provide a framework for certifying proofs given in such calculi. The method is based on the use of a translation from the modal language into a first-order polarized language and on a checker whose trusted kernel is a simple implementation of a classical focused sequent calculus. The framework allows for a high flexibility in the representation of proofs to be checked, in the sense that even partial proofs can be verified by employing a process of proof reconstruction. We describe the general method for modal logics characterized by geometric frame conditions, present its implementation in a Prolog-like language, and provide several examples of proof certification in the case of well-known normal modal logics, like K, S4 and S5
A general proof certification framework for modal logic
No full textOne of the main issues in proof certification is that different theorem provers, even when designed for the same logic, tend to use different proof formalisms and to produce outputs in different formats. The project ProofCert promotes the usage of a common specification language and of a small and trusted kernel in order to check proofs coming from different sources and for different logics. By relying on that idea and by using a classical focused sequent calculus as a kernel, we propose here a general framework for checking modal proofs. We present the implementation of the framework in a prolog-like language and show how it is possible to specialize it in a simple and modular way in order to cover different proof formalisms, such as labeled systems, tableaux, sequent calculi and nested sequent calculi. We illustrate the method for the logic K by providing several examples and discuss how to further extend the approach
- …
