1,721,264 research outputs found
Intelligent Computer Mathematics - 14th International Conference, CICM 2021, Timisoara, Romania, July 26–31, 2021, Proceedings
No full textWith the continuing, rapid progress of digital methods in communications, knowledge
representation, processing, and discovery, the unique character and needs of mathematical information require unique approaches. Its specialized representations and
capacity for creation and proof, both automatically and formally as well as manually,
set mathematical knowledge apart.
The Conference on Intelligent Computer Mathematics (CICM) was initially formed
in 2008 as a joint meeting of communities involved in computer algebra systems,
automated theorem provers, and mathematical knowledge management, as well as
those involved in a variety of aspects of scientific document archives. It has offered a
venue for discussing, developing, and integrating the diverse, sometimes eclectic,
approaches and research. Since 2008, CICM has been held annually: Birmingham (UK,
2008), Grand Bend (Canada, 2009), Paris (France, 2010), Bertinoro (Italy, 2011),
Bremen (Germany, 2012), Bath (UK, 2013), Coimbra (Portugal, 2014),
Washington D. C. (USA, 2015), Bialystok (Poland, 202016), Edinburgh (UK, 2017),
Linz (Austria, 2018), Prague (Czech Republic, 2019) and Bertinoro (Italy, 2020). This
latter edition, which was originally scheduled to be held in Bertinoro, Italy, was hosted
online due to the COVID-19 pandemic. This year’s meeting was supposed to be held in
Timisoara, Romania, but again due to the pandemic, it was held online (July 26–31,
2021).
This year’s meeting exposed advances in formalizations, automatic theorem proving, applications of machine learning to mathematical documents and proof search,
search and classifications of mathematical documents, teaching and geometric reasoning, and logic and systems, among other topics. This volume contains the contributions to this conference. From 38 formal submissions, the Program Committee
(PC) accepted 20 papers including 12 full research papers, 7 shorter papers describing
software systems or datasets and 1 paper highlighting development of systems and
tools in the last year. All papers were reviewed by at least three PC members or
external reviewers. The reviews were single-blind and included a response period in
which the authors could respond and clarify points raised by the reviewers. In addition
to the main sessions, the conference included a doctoral program, chaired by Yasmine
Sharoda, which provided a forum for PhD students to present their research and get
advice from senior members of the community. Additionally, the following workshops
were scheduled:
– The 31st OpenMath Workshop, organized by James Davenport and Michael
Kohlhase.
– The 2nd Workshop on Natural Formal Mathematics (NatFoM 2021), organized
by Peter Koepke and Dennis Müller.
– The 5th Workshop on Formal Mathematics for Mathematicians (FMM 2021),
organized by Jasmine Blanchette and Adam Naumowicz.
– The 2nd Workshop on Formal Verification of Physical Systems (FVPS 2021),
organized by Sofiene Tahar, Osman Hasan and Adnan Rashid.
– The 13th Workshop on Mathematical User Interaction (MathUI 2021), organized by
Andrea Kohlhase.
Finally, the conference included four invited talks:
– Alessandro Cimatti (Fondazione Bruno Kessler, Italy): “Logic at work, and some
research challenges for computer mathematics”.
– Michael Kohlhase (FAU Erlangen-Nürnberg, Germany): “Referential Semantics – a
Concept for Bridging between Representations of mathematical/technical Documents and Knowledge”.
– Laura Kovacs (TU Vienna, Austria): “Induction in Saturation-Based Reasoning”.
– Angus McIntyre (Emeritus Professor, Queen Mary University of London, UK):
“Doing classical number theory in weak axiomatic systems”.
A successful conference is due to the efforts of many people. We thank Madalina
Erascu and her colleagues at the West University of Timisoara, Romania, for the
difficult task of organizing a conference with the expectation of it being held face to
face but with the dynamics of COVID-19 making it difficult to accommodate in person
meetings. We are grateful to Serge Autexier for his publicity work. We also thank the
authors of submitted papers, the PC for their reviews, and the organizers of the
workshops, as well as the invited speakers and the participants of the conference.
June 2021 F. Kamareddine
C. Sacerdoti Coe
A Plugin to Export Coq Libraries to XML
No full textWe introduce a plugin for the interactive prover Coq to export its libraries to a machine readable XML format. The information exported is the one checked by Coq’s kernel after the input is elaborated, augmented with additional data coming from the elaboration itself. The plugin has been applied to the 49 Coq libraries that have an opam package and that currently compile with the latest version of Coq (8.9.0), generating a large dataset of 1,235,934 compressed XML files organized in 18,780 directories that require 17Â GB on disk
Properties of a Computational Lambda Calculus for Higher-Order Relational Queries
Get PDFWe study the operational semantics of an untyped computational lambda calculus whose normal forms represent queries on databases. The calculus extends the computational core with additional operations and rewriting rules whose effect is to turn the monadic type of computations into a multiset monad that captures tables. Moreover, we introduce comonadic constructs and additional rewriting rules to be able to form tables of tables. Proving confluence becomes tricky: we succeed exploiting decreasing diagrams. In the second part, we study a Curry style type assignment system for the calculus. We introduce an idempotent intersection type system establishing type invariance under conversion
The Coq Library as a Theory Graph
No full textRepresenting proof assistant libraries in a way that allows further processing in other systems is becoming increasingly important. It is a critical missing link for integrating proof assistants both with each other or with peripheral tools such as IDEs or proof checkers. Such representations cannot be generated from library source files because they lack semantic enrichment (inferred types, etc.) and only the original proof assistant is able to process them. But even when using the proof assistant’s internal data structures, the complexities of logic, implementation, and library still make this very difficult. We describe one such representation, namely for the library of Coq, using OMDoc theory graphs as the target format. Coq is arguably the most formidable of all proof assistant libraries to tackle, and our work makes a significant step forward. On the theoretical side, our main contribution is a translation of the Coq module system into theory graphs. This greatly reduces the complexity of the library as the more arcane module system features are eliminated while preserving most of the structure. On the practical side, our main contribution is an implementation of this translation. It takes the entire Coq library, which is split over hundreds of decentralized repositories, and produces easily-reusable OMDoc files as output
Implementing type theory in higher order constraint logic programming
No full textIn this paper, we are interested in high-level programming languages to implement the core components of an interactive theorem prover for a dependently typed language: the kernel - responsible for type-checking closed terms - and the elaborator - that manipulates open terms, that is terms containing unresolved unification variables.In this paper, we confirm that rolog, the language developed by Miller and Nadathur since the 80s, is extremely suitable for implementing the kernel. Indeed, we easily obtain a type checker for the Calculus of Inductive Constructions (CIC). Even more, we do so in an incremental way by escalating a checker for a pure type system to the full CIC.We then turn our attention to the elaborator with the objective to obtain a simple implementation thanks to the features of the programming language. In particular, we want to use Prolog's unification variables to model the object language ones. In this way, scope checking, carrying of assignments and occur checking are handled by the programming language.We observe that the eager generative semantics inherited from Prolog clashes with this plan. We propose an extension to Prolog that allows to control the generative semantics, suspend goals over flexible terms turning them into constraints, and finally manipulate these constraints at the meta-meta level via constraint handling rules.We implement the proposed language extension in the Embedded Lambda Prolog Interpreter system and we discuss how it can be used to extend the kernel into an elaborator for CIC
Going Beyond Counting First Authors in Author Co-citation Analysis
Get PDFThe 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
"Non nominare il nome di Dio invano"
No full textPrendendo le mosse dall'oltraggiosa adozione nazista del motto Gott mit uns, "Non nominare il nome di Dio invano" è un saggio linguistico-fonetico sul Nome Divino che, attraverso la descrizione fonetica e alcuni degli innumerevoli tratti semantici del Tetragramma, ne esplora l'essenza, cercando di mostrare con le istanze del Credo biblico il paradosso dello sterminio nazista e rivendicando il ruolo e il posto della fede nella scienza come strumento di osservazione e di analisi, nonché possibile e credibile chiave di lettura nella ricerca di risposte di senso sulla realtà che ci circonda
- …
