A Comprehensive Framework for Saturation Theorem Proving.
Automated theorem proving
Prover architectures
Redundancy
Resolution calculus
Saturation
Superposition calculus
Journal
Journal of automated reasoning
ISSN: 1573-0670
Titre abrégé: J Autom Reason
Pays: Netherlands
ID NLM: 101730032
Informations de publication
Date de publication:
2022
2022
Historique:
received:
28
05
2021
accepted:
21
03
2022
entrez:
10
11
2022
pubmed:
11
11
2022
medline:
11
11
2022
Statut:
ppublish
Résumé
A crucial operation of saturation theorem provers is deletion of subsumed formulas. Designers of proof calculi, however, usually discuss this only informally, and the rare formal expositions tend to be clumsy. This is because the equivalence of dynamic and static refutational completeness holds only for derivations where all deleted formulas are redundant, but the standard notion of redundancy is too weak: A clause
Identifiants
pubmed: 36353684
doi: 10.1007/s10817-022-09621-7
pii: 9621
pmc: PMC9637109
doi:
Types de publication
Journal Article
Langues
eng
Pagination
499-539Informations de copyright
© The Author(s) 2022.