Lataa...

Subsumption Demodulation in First-Order Theorem Proving

Motivated by applications of first-order theorem proving to software analysis, we introduce a new inference rule, called subsumption demodulation, to improve support for reasoning with conditional equalities in superposition-based theorem proving. We show that subsumption demodulation is a simplific...

Täydet tiedot

Tallennettuna:
Bibliografiset tiedot
Julkaisussa:Automated Reasoning
Päätekijät: Gleiss, Bernhard, Kovács, Laura, Rath, Jakob
Aineistotyyppi: Artigo
Kieli:Inglês
Julkaistu: 2020
Aiheet:
Linkit:https://ncbi.nlm.nih.gov/pmc/articles/PMC7324223/
https://ncbi.nlm.nih.govhttp://dx.doi.org/10.1007/978-3-030-51074-9_17
Tagit: Lisää tagi
Ei tageja, Lisää ensimmäinen tagi!