Top 5 Arxiv Papers Today in Logic In Computer Science


2.04 Mikeys
#1. Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
Qingxiang Wang, Chad Brown, Cezary Kaliszyk, Josef Urban
In this paper we share several experiments trying to automatically translate informal mathematics into formal mathematics. In our context informal mathematics refers to human-written mathematical sentences in the LaTeX format; and formal mathematics refers to statements in the Mizar language. We conducted our experiments against three established neural network-based machine translation models that are known to deliver competitive results on translating between natural languages. To train these models we also prepared four informal-to-formal datasets. We compare and analyze our results according to whether the model is supervised or unsupervised. In order to augment the data available for auto-formalization and improve the results, we develop a custom type-elaboration mechanism and integrate it in the supervised translation.
more | pdf | html
Figures
None.
Tweets
arxivml: "Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar", Qingxiang Wang, Chad Brow… https://t.co/T5pZwgpcDj
arxiv_cs_LG: Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar. Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban https://t.co/sImRlzaM8n
Memoirs: Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar. https://t.co/34tXS1wpis
arxiv_cscl: Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar https://t.co/xlrBoDnN90
arxiv_cscl: Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar https://t.co/xlrBoDnN90
arxiv_cscl: Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar https://t.co/xlrBoDnN90
arxiv_cslo: Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar https://t.co/fLeCreNQx8
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 4
Total Words: 0
Unqiue Words: 0

2.003 Mikeys
#2. Game Description Logic with Integers: A GDL Numerical Extension
Munyque Mittelmann, Laurent Perrussel
Many problems can be viewed as games, where one or more agents try to ensure that certain objectives hold no matter the behavior from the environment and other agents. In recent years, a number of logical formalisms have been proposed for specifying games among which the Game Description Language (GDL) was established as the official language for General Game Playing. Although numbers are recurring in games, the description of games with numerical features in GDL requires the enumeration from all possible numeric values and the relation among them. Thereby, in this paper, we introduce the Game Description Logic with Integers (GDLZ) to describe games with numerical variables, numerical parameters, as well as to perform numerical comparisons. We compare our approach with GDL and show that when describing the same game, GDLZ is more compact.
more | pdf | html
Figures
None.
Tweets
arxivml: "Game Description Logic with Integers: A GDL Numerical Extension", Munyque Mittelmann, Laurent Perrussel https://t.co/VxnILzjgoR
SciFi: Game Description Logic with Integers: A GDL Numerical Extension. https://t.co/pGakmaPwgp
arxiv_cslo: Game Description Logic with Integers: A GDL Numerical Extension https://t.co/YDwXNI81fn
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 2
Total Words: 0
Unqiue Words: 0

1.999 Mikeys
#3. A Quantitative Understanding of Pattern Matching
Sandra Alves, Delia Kesner, Daniel Ventura
This paper shows that the recent approach to quantitative typing systems for programming languages can be extended to pattern matching features. Indeed, we define two resource aware type systems, named U and E, for a lambda-calculus equipped with pairs for both patterns and terms. Our typing systems borrow some basic ideas from [BKRDR15], which characterises (head) normalisation in a qualitative way, in the sense that typability and normalisation coincide. But in contrast to [BKRDR15], our (static) systems also provides quantitative information about the dynamics of the calculus. Indeed, system U provides upper bounds for the length of normalisation sequences plus the size of their corresponding normal forms, while system E, which can be seen as a refinement of system U, produces exact bounds for each of them. This is achieved by means of a non-idempotent intersection type system equipped with different technical tools. First of all, we use product types to type pairs, instead of the disjoint unions in [BKRDR15], thus avoiding an...
more | pdf | html
Figures
None.
Tweets
arxiv_cslo: A Quantitative Understanding of Pattern Matching https://t.co/4ayoVSZzrz
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 3
Total Words: 20870
Unqiue Words: 2848

1.999 Mikeys
#4. A Constructive Formalization of the Weak Perfect Graph Theorem
Abhishek Kr Singh, Raja Natarajan
The Perfect Graph Theorems are important results in graph theory describing the relationship between clique number $\omega(G) $ and chromatic number $\chi(G) $ of a graph $G$. A graph $G$ is called \emph{perfect} if $\chi(H)=\omega(H)$ for every induced subgraph $H$ of $G$. The Strong Perfect Graph Theorem (SPGT) states that a graph is perfect if and only if it does not contain an odd hole (or an odd anti-hole) as its induced subgraph. The Weak Perfect Graph Theorem (WPGT) states that a graph is perfect if and only if its complement is perfect. In this paper, we present a formal framework for working with finite simple graphs. We model finite simple graphs in the Coq Proof Assistant by representing its vertices as a finite set over a countably infinite domain. We argue that this approach provides a formal framework in which it is convenient to work with different types of graph constructions (or expansions) involved in the proof of the Lov\'{a}sz Replication Lemma (LRL), which is also the key result used in the proof of Weak...
more | pdf | html
Figures
None.
Tweets
arxiv_cslo: A Constructive Formalization of the Weak Perfect Graph Theorem https://t.co/Hp92wppV6j
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 2
Total Words: 9932
Unqiue Words: 1831

1.999 Mikeys
#5. The Expressiveness of Looping Terms in the Semantic Programming
Sergey Goncharov, Sergey Ospichev, Denis Ponomaryov, Dmitry Sviridenko
We consider the complexity of reasoning in extensions of the language of $\Delta_0$-formulas with non-standard list terms, which represent bounded list search, bounded recursion, and bounded iteration. We provide a number of complexity bounds on model checking and satisfiability for these formulas. In particular, we show that the set of $\Delta_0$-formulas with bounded recursive terms true in a given list superstructure $HW(\mathcal{M})$ is non-elementary (i.e., it contains the class kEXPTIME, for all $k\geqslant 1$). For $\Delta_0$-formulas with bounded iteration or restricted usage of recursive terms, we show lower complexity.
more | pdf | html
Figures
None.
Tweets
arxiv_cslo: The Expressiveness of Looping Terms in the Semantic Programming https://t.co/mc4R2psTye
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 4
Total Words: 0
Unqiue Words: 0

About

Assert is a website where the best academic papers on arXiv (computer science, math, physics), bioRxiv (biology), BITSS (reproducibility), EarthArXiv (earth science), engrXiv (engineering), LawArXiv (law), PsyArXiv (psychology), SocArXiv (social science), and SportRxiv (sport research) bubble to the top each day.

Papers are scored (in real-time) based on how verifiable they are (as determined by their Github repos) and how interesting they are (based on Twitter).

To see top papers, follow us on twitter @assertpub_ (arXiv), @assert_pub (bioRxiv), and @assertpub_dev (everything else).

To see beautiful figures extracted from papers, follow us on Instagram.

Tracking 234,443 papers.

Search
Sort results based on if they are interesting or reproducible.
Interesting
Reproducible
Categories
All
Astrophysics
Cosmology and Nongalactic Astrophysics
Earth and Planetary Astrophysics
Astrophysics of Galaxies
High Energy Astrophysical Phenomena
Instrumentation and Methods for Astrophysics
Solar and Stellar Astrophysics
Condensed Matter
Disordered Systems and Neural Networks
Mesoscale and Nanoscale Physics
Materials Science
Other Condensed Matter
Quantum Gases
Soft Condensed Matter
Statistical Mechanics
Strongly Correlated Electrons
Superconductivity
Computer Science
Artificial Intelligence
Hardware Architecture
Computational Complexity
Computational Engineering, Finance, and Science
Computational Geometry
Computation and Language
Cryptography and Security
Computer Vision and Pattern Recognition
Computers and Society
Databases
Distributed, Parallel, and Cluster Computing
Digital Libraries
Discrete Mathematics
Data Structures and Algorithms
Emerging Technologies
Formal Languages and Automata Theory
General Literature
Graphics
Computer Science and Game Theory
Human-Computer Interaction
Information Retrieval
Information Theory
Machine Learning
Logic in Computer Science
Multiagent Systems
Multimedia
Mathematical Software
Numerical Analysis
Neural and Evolutionary Computing
Networking and Internet Architecture
Other Computer Science
Operating Systems
Performance
Programming Languages
Robotics
Symbolic Computation
Sound
Software Engineering
Social and Information Networks
Systems and Control
Economics
Econometrics
General Economics
Theoretical Economics
Electrical Engineering and Systems Science
Audio and Speech Processing
Image and Video Processing
Signal Processing
General Relativity and Quantum Cosmology
General Relativity and Quantum Cosmology
High Energy Physics - Experiment
High Energy Physics - Experiment
High Energy Physics - Lattice
High Energy Physics - Lattice
High Energy Physics - Phenomenology
High Energy Physics - Phenomenology
High Energy Physics - Theory
High Energy Physics - Theory
Mathematics
Commutative Algebra
Algebraic Geometry
Analysis of PDEs
Algebraic Topology
Classical Analysis and ODEs
Combinatorics
Category Theory
Complex Variables
Differential Geometry
Dynamical Systems
Functional Analysis
General Mathematics
General Topology
Group Theory
Geometric Topology
History and Overview
Information Theory
K-Theory and Homology
Logic
Metric Geometry
Mathematical Physics
Numerical Analysis
Number Theory
Operator Algebras
Optimization and Control
Probability
Quantum Algebra
Rings and Algebras
Representation Theory
Symplectic Geometry
Spectral Theory
Statistics Theory
Mathematical Physics
Mathematical Physics
Nonlinear Sciences
Adaptation and Self-Organizing Systems
Chaotic Dynamics
Cellular Automata and Lattice Gases
Pattern Formation and Solitons
Exactly Solvable and Integrable Systems
Nuclear Experiment
Nuclear Experiment
Nuclear Theory
Nuclear Theory
Physics
Accelerator Physics
Atmospheric and Oceanic Physics
Applied Physics
Atomic and Molecular Clusters
Atomic Physics
Biological Physics
Chemical Physics
Classical Physics
Computational Physics
Data Analysis, Statistics and Probability
Physics Education
Fluid Dynamics
General Physics
Geophysics
History and Philosophy of Physics
Instrumentation and Detectors
Medical Physics
Optics
Plasma Physics
Popular Physics
Physics and Society
Space Physics
Quantitative Biology
Biomolecules
Cell Behavior
Genomics
Molecular Networks
Neurons and Cognition
Other Quantitative Biology
Populations and Evolution
Quantitative Methods
Subcellular Processes
Tissues and Organs
Quantitative Finance
Computational Finance
Economics
General Finance
Mathematical Finance
Portfolio Management
Pricing of Securities
Risk Management
Statistical Finance
Trading and Market Microstructure
Quantum Physics
Quantum Physics
Statistics
Applications
Computation
Methodology
Machine Learning
Other Statistics
Statistics Theory
Feedback
Online
Stats
Tracking 234,443 papers.