Towards a Unified Ordering for Superposition-based Automated Reasoning

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F18%3A00329376" target="_blank" >RIV/68407700:21730/18:00329376 - isvavai.cz</a>

Výsledek na webu

<a href="https://link.springer.com/chapter/10.1007/978-3-319-96418-8_29" target="_blank" >https://link.springer.com/chapter/10.1007/978-3-319-96418-8_29</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-96418-8_29" target="_blank" >10.1007/978-3-319-96418-8_29</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Towards a Unified Ordering for Superposition-based Automated Reasoning

Popis výsledku v původním jazyce

We propose an extension of the automated theorem prover E by the weighted path ordering. Weighted path ordering is theoretically stronger than all the orderings used in E-prover, however its parametrization is more involved than those normally used in automated reasoning. In particular, it depends on a term algebra. We discuss how the parameters for the ordering can be proposed automatically for particular theorem proving problem strategies. We integrate the ordering in E-prover and perform an evaluation on the standard theorem proving benchmarks. The ordering is complementary to the ones used in E prover so far.

Název v anglickém jazyce

Towards a Unified Ordering for Superposition-based Automated Reasoning

Popis výsledku anglicky

We propose an extension of the automated theorem prover E by the weighted path ordering. Weighted path ordering is theoretically stronger than all the orderings used in E-prover, however its parametrization is more involved than those normally used in automated reasoning. In particular, it depends on a term algebra. We discuss how the parameters for the ordering can be proposed automatically for particular theorem proving problem strategies. We integrate the ordering in E-prover and perform an evaluation on the standard theorem proving benchmarks. The ordering is complementary to the ones used in E prover so far.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

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

Projekt

—

Návaznosti

R - Projekt Ramcoveho programu EK

Rok uplatnění

2018

Kód důvěrnosti údajů

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

Název statě ve sborníku

Mathematical Software – ICMS 2018

ISBN

978-3-319-96417-1

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

10

Strana od-do

245-254

Název nakladatele

Springer

Místo vydání

Basel

Místo konání akce

South Bend

Datum konání akce

24. 7. 2018

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000455774600029