This article is a tribute to the scientific legacy of automated reasoning pioneer and JAR founder Lawrence T. (Larry) Wos. Larry's main technical contributions were the set-of-support strategy for resolution theorem proving, and the demodulation and paramodulation inference rules for building equality into resolution. Starting from the original definitions of these concepts in Larry's papers, this survey traces their evolution, unearthing the often forgotten trails that connect Larry's original definitions to those that became standard in the field.

Set of support, demodulation, paramodulation: a historical perspective

Maria Paola Bonacina
2022-01-01

Abstract

This article is a tribute to the scientific legacy of automated reasoning pioneer and JAR founder Lawrence T. (Larry) Wos. Larry's main technical contributions were the set-of-support strategy for resolution theorem proving, and the demodulation and paramodulation inference rules for building equality into resolution. Starting from the original definitions of these concepts in Larry's papers, this survey traces their evolution, unearthing the often forgotten trails that connect Larry's original definitions to those that became standard in the field.
Resolution, Set of Support, Demodulation, Paramodulation
File in questo prodotto:
File Dimensione Formato  
WosHistoricSurvey-JARversion.pdf

accesso aperto

Descrizione: Articolo principale
Tipologia: Versione dell'editore
Licenza: Creative commons
Dimensione 643.11 kB
Formato Adobe PDF
643.11 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/1061136
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
social impact