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
None.

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

None.

None.

Sample Sizes : None.

Authors: 4

Total Words: 0

Unqiue Words: 0

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
None.

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

None.

None.

Sample Sizes : None.

Authors: 2

Total Words: 0

Unqiue Words: 0

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
None.

arxiv_cslo:
A Quantitative Understanding of Pattern Matching https://t.co/4ayoVSZzrz

None.

None.

Sample Sizes : None.

Authors: 3

Total Words: 20870

Unqiue Words: 2848

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
None.

arxiv_cslo:
A Constructive Formalization of the Weak Perfect Graph Theorem https://t.co/Hp92wppV6j

None.

None.

Sample Sizes : None.

Authors: 2

Total Words: 9932

Unqiue Words: 1831

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
None.

arxiv_cslo:
The Expressiveness of Looping Terms in the Semantic Programming https://t.co/mc4R2psTye

None.

None.

Sample Sizes : None.

Authors: 4

Total Words: 0

Unqiue Words: 0

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.*

Sort results based on if they are interesting or reproducible.

Interesting

Reproducible