Layered Clause Selection for Saturation-Based Theorem Proving

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F20%3A00344481" target="_blank" >RIV/68407700:21730/20:00344481 - isvavai.cz</a>

Result on the web

<a href="http://ceur-ws.org/Vol-2752/paper3.pdf" target="_blank" >http://ceur-ws.org/Vol-2752/paper3.pdf</a>

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Layered Clause Selection for Saturation-Based Theorem Proving

Original language description

Clause selection is one of the main heuristic decision points in navigating proof search of saturationbased theorem provers. A recently developed layered clause selection framework allows one to boost a basic clause selection heuristic by organising clauses into groups of more or less promising ones according to a specified numerical feature. In this work, we investigate this framework in depth and introduce, in addition to a previously presented feature (based on the amount of theory reasoning in the derivation of a clause), three new features for clause selection (tracking relatedness to the goal, the number of split dependencies in the Avatar architecture, and closeness to the Horn fragment, respectively). We implemented the resulting clause selection heuristics in the state-of-the-art saturation-based theorem prover Vampire and present an evaluation of these new clause-selection strategies and their combinations over the TPTP and SMTLIB libraries.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

<a href="/en/project/GJ20-06390Y" target="_blank" >GJ20-06390Y: Powering Automatic Theorem Provers by Machine Learning</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2020

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Practical Aspects of Automated Reasoning and Satisfiability Checking and Symbolic Computation Workshop 2020

ISBN

—

ISSN

1613-0073

e-ISSN

1613-0073

Number of pages

19

Pages from-to

34-52

Publisher name

CEUR Workshop Proceedings

Place of publication

Tilburg

Event location

Paris

Event date

Jun 29, 2020

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—