Yüklüyor......

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...

Ful tanımlama

Kaydedildi:
Detaylı Bibliyografya
Yayımlandı:Automated Reasoning
Asıl Yazarlar: Gleiss, Bernhard, Kovács, Laura, Rath, Jakob
Materyal Türü: Artigo
Dil:Inglês
Baskı/Yayın Bilgisi: 2020
Konular:
Online Erişim:https://ncbi.nlm.nih.gov/pmc/articles/PMC7324223/
https://ncbi.nlm.nih.govhttp://dx.doi.org/10.1007/978-3-030-51074-9_17
Etiketler: Etiketle
Etiket eklenmemiş, İlk siz ekleyin!