Superposition with Lambdas

Autor: Bentkamp, Alexander, Blanchette, Jasmin, Tourret, Sophie, Vukmirović, Petar, Waldmann, Uwe

We designed a superposition calculus for a clausal fragment of extensional polymorphic higher-order logic that includes anonymous functions but excludes Booleans. The inference rules work on $\beta\eta$-equivalence classes of $\lambda$-terms and rely

Externí odkaz: http://arxiv.org/abs/2102.00453

Logical reduction of metarules

Autor: Cropper, Andrew, Tourret, Sophie

Many forms of inductive logic programming (ILP) use \emph{metarules}, second-order Horn clauses, to define the structure of learnable programs and thus the hypothesis space. Deciding which metarules to use for a given learning task is a major open pr

Externí odkaz: http://arxiv.org/abs/1907.10952

Mechanical Mathematicians.

Autor: BENTKAMP, ALEXANDER, BLANCHETTE, JASMIN, NUMMELIN, VISA, TOURRET, SOPHIE, VUKMIROVIĆ, PETAR, WALDMANN, UWE

Publikováno v: Communications of the ACM; Apr2023, Vol. 66 Issue 4, p80-90, 11p, 2 Color Photographs, 2 Diagrams, 1 Chart

Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.

A Comprehensive Framework for Saturation Theorem Proving

Autor: Waldmann, Uwe, Tourret, Sophie, Robillard, Simon, Blanchette, Jasmin, Peltier, Nicolas, Sofronie-Stokkermans, Viorica

Publikováno v: Journal of Automated Reasoning, 66(4), 499-539. Springer Netherlands
IJCAR 2020 (Part I) International Joint Conference on Automated Reasoning
IJCAR 2020 (Part I) International Joint Conference on Automated Reasoning, Jun 2020, Paris, France. pp.316-334, ⟨10.1007/978-3-030-51074-9_18⟩
Waldmann, U, Tourret, S, Robillard, S & Blanchette, J 2020, A Comprehensive Framework for Saturation Theorem Proving . in N Peltier & V Sofronie-Stokkermans (eds), Automated Reasoning : 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I . vol. 1, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12166 LNAI, Springer, pp. 316-334, 10th International Joint Conference on Automated Reasoning, IJCAR 2020, Virtual, Online, 1/07/20 . https://doi.org/10.1007/978-3-030-51074-9_18
Automated Reasoning-10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Automated Reasoning
Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I, 1, 316-334
Waldmann, U, Tourret, S, Robillard, S & Blanchette, J 2022, ' A Comprehensive Framework for Saturation Theorem Proving ', Journal of Automated Reasoning, vol. 66, no. 4, pp. 499-539 . https://doi.org/10.1007/s10817-022-09621-7
Automated Reasoning ISBN: 9783030510732
IJCAR (1)
Journal of Automated Reasoning
Journal of Automated Reasoning, 2022, 66 (4), pp.499-539. ⟨10.1007/s10817-022-09621-7⟩
Automated Reasoning

A crucial operation of saturation theorem provers is deletion of subsumed formulas. Designers of proof calculi, however, usually discuss this only informally, and the rare formal expositions tend to be clumsy. This is because the equivalence of dynam

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9ce4f636ee6aa8cdff07937ea4a58d35
https://research.vu.nl/en/publications/04fbca2a-c66f-4cee-a1a1-bca932a6ff60