Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Journal of Automated Reasoning
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

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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 haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

  • über 102.000 Bücher
  • über 537 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 Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

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




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

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




 

Jetzt Wissensvorsprung sichern!

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

Pardinus: A Temporal Relational Model Finder

OriginalPaper

A Formalization of SQL with Nulls

Correction

Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic

OriginalPaper

Theorem Proving as Constraint Solving with Coherent Logic

OriginalPaper

Fast Left Kan Extensions Using the Chase

OriginalPaper

A Comprehensive Framework for Saturation Theorem Proving

Premium Partner

    Bildnachweise