Skip to main content
Registrieren
Springer Professional
SUCHE
MENÜ 1 2 3 4
nach oben

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Erschienen in: Journal of Automated Reasoning 4/2022

09.01.2022

A Wos Challenge Met

verfasst von: Robert Veroff

Erschienen in: Journal of Automated Reasoning | Ausgabe 4/2022

Einloggen, um Zugang zu erhalten
share
TEILEN

Abstract

In his regular column in the AAR Newsletter, Larry Wos typically posed challenges to the automated reasoning community. Some of these challenges concern general research objectives, but several of them concern specific problems relevant to his own experience and attempts to solve especially difficult problems, including open questions, with an automated theorem prover. This note honors Larry’s memory by working through a solution to one of these challenges.
Vorheriger Artikel Making Higher-Order Superposition Work
Nächster Artikel A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 69.000 Bücher
  • über 500 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 58.000 Bücher
  • über 300 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko





Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 50.000 Bücher
  • über 380 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe



 


Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren
Fußnoten
1
Larry also mentions an interest in having derivations of the goal clauses that are equality ordered exactly as given in the problem description. Comments about this aspect of the challenge are included at the end of this article.
 
Literatur
1.
Anantharaman, S., Hsiang, J.: Automated proofs of the Moufang identities in alternative rings. J. Autom. Reason. 6(1), 79–109 (1990) MathSciNetCrossRefMATH
2.
Bonacina, M. P.: Combination of distributed search and multi-search in Peers-mcd.d. In R. P. Gore, A. Leitsch and T. Nipkow (eds), Proceedings of the First International Joint Conference on Automated Reasoning (IJCAR), LNCS (LNAI) 2083:448–452, Springer (2001)
3.
Kinyon, M., Veroff, R., Vojtěchovský, P.: Loops with abelian inner mapping groups: an application of automated deduction. In: Bonacina, M.P., Stickel, M. (eds.) Automated reasoning and mathematics: essays in memory of William W McCune, LNCS (LNAI), pp. 151–164. Springer, Berlin (2013) CrossRef
4.
5.
6.
7.
8.
Veroff, R.: Using hints to increase the effectiveness of an automated reasoning program: case studies. J. Autom. Reason. 16(3), 223–239 (1996) MathSciNetCrossRefMATH
9.
Veroff, R.: Solving open questions and other challenge problems using proof sketches. J. Autom. Reason. 27(2), 157–174 (2001) MathSciNetCrossRefMATH
10.
11.
12.
13.
Metadaten
Titel
A Wos Challenge Met
verfasst von
Robert Veroff
Publikationsdatum
09.01.2022
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 4/2022
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-021-09614-y

Weitere Artikel der Ausgabe 4/2022

Journal of Automated Reasoning 4/2022 Zur Ausgabe

OriginalPaper

Theorem Proving as Constraint Solving with Coherent Logic

OriginalPaper

Set of Support, Demodulation, Paramodulation: A Historical Perspective

OriginalPaper

Pardinus: A Temporal Relational Model Finder

OriginalPaper

A Formalization of SQL with Nulls

OriginalPaper

Fast Left Kan Extensions Using the Chase

OriginalPaper

A Comprehensive Framework for Saturation Theorem Proving

Premium Partner