Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers

Autor: Mangla, C, Holden, SB, Paulson, LC

Astrategy scheduleallocates time to proof strategies that are used in sequence in a theorem prover. We employ Bayesian statistics to propose alternative sequences for the strategy schedule in each proof attempt. Tested on the TPTP problem library, ou

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::6a0eea2f23062d3fc6f70715d09366da

A Modular First Formalisation of Combinatorial Design Theory

Autor: Edmonds, C, Paulson, LC

Publikováno v: Lecture Notes in Computer Science
Lecture Notes in Computer Science-Intelligent Computer Mathematics
Lecture Notes in Computer Science ISBN: 9783030810962
CICM
Intelligent Computer Mathematics-14th International Conference, CICM 2021, Timisoara, Romania, July 26–31, 2021, Proceedings

Combinatorial design theory studies set systems with certain balance and symmetry properties and has applications to computer science and elsewhere. This paper presents a modular approach to formalising designs for the first time using Isabelle and a

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4b6abd4a4052fbdc02a51c407a63138a
http://arxiv.org/abs/2105.13583

Bayesian optimisation of solver parameters in CBMC

Autor: Mangla, C, Holden, SB, Paulson, LC

Satisfiability solvers can be embedded in applications to perform specific formal reasoning tasks. CBMC, for example, is a bounded model checker for C and C++ that embeds SMT and SAT solvers to check internally generated formulae. Such solvers will b

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::bf268aa15047d1e91826a185b000616e

A simple formalization and proof for the mutilated chess board.

Autor: Paulson, LC¹

Publikováno v: Logic Journal of the IGPL. 2000, Vol. 9 Issue 3, p475-485. 11p.

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