104,727 research outputs found
Proof Terms for Generalized Natural Deduction
No full textIn previous work it has been shown how to generate natural deduction rules for propositional connectives from truth tables, both for classical and constructive logic. The present paper extends this for the constructive case with proof-terms, thereby extending the Curry-Howard isomorphism to these new connectives. A general notion of conversion of proofs is defined, both as a conversion of derivations and as a reduction of proof-terms. It is shown how the well-known rules for natural deduction (Gentzen, Prawitz) and general elimination rules (Schroeder-Heister, von Plato, and others), and their proof conversions can be found as instances. As an illustration of the power of the method, we give constructive rules for the nand logical operator (also called Sheffer stroke).
As usual, conversions come in two flavours: either a detour conversion arising from a detour convertibility, where an introduction rule is immediately followed by an elimination rule, or a permutation conversion arising from an permutation convertibility, an elimination rule nested inside another elimination rule. In this paper, both are defined for the general setting, as conversions of derivations and as reductions of proof-terms. The properties of these are studied as proof-term reductions. As one of the main contributions it is proved that detour conversion is strongly normalizing and permutation conversion is strongly normalizing: no matter how one reduces, the process eventually terminates. Furthermore, the combination of the two conversions is shown to be weakly normalizing: one can always reduce away all convertibilities
Iteration and primitive recursion in categorical terms
No full textContains fulltext :
34575.pdf ( ) (Open Access
Characteristics of de Bruijn's early proof checker Automath
No full textThe `mathematical language' Automath, conceived by N.G. de Bruijn in 1968,
was the first theorem prover actually working and was used for checking many
specimina of mathematical content. Its goals and syntactic ideas inspired Th.
Coquand and G. Huet to develop the calculus of constructions, CC, which was one
of the first widely used interactive theorem provers and forms the basis for
the widely used Coq system. The original syntax of Automath is not easy to
grasp. Yet, it is essentially based on a derivation system that is similar to
the Calculus of Constructions (`CC'). The relation between the Automath syntax
and CC has not yet been sufficiently described, although there are many
references in the type theory community to Automath. In this paper we focus on
the backgrounds and on some uncommon aspects of the syntax of Automath. We
expose the fundamental aspects of a `generic' Automath system, encapsulating
the most common versions of Automath. We present this generic Automath system
in a modern syntactic frame. The obtained system makes use of {\lambda}D, a
direct extension of CC with definitions
A Real Semantic Web for Mathematics Deserves a Real Semantics
No full textContains fulltext :
72735.pdf (author's version ) (Open Access)SemWiki 2008, 02 juni 200
Front Matter, Table of Contents, Preface, Conference Organization
No full textFront Matter, Table of Contents, Preface, Conference Organizatio
Going Beyond Counting First Authors in Author Co-citation Analysis
No full textThe 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
An Interactive Algebra Course with Formalised Proofs and Definitions
No full textContains fulltext :
36143.pdf (author's version ) (Open Access)MKM 200
Appropriate Similarity Measures for Author Cocitation Analysis
No full textWe 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
- …
