Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Journal of Automated Reasoning
Published in: Journal of Automated Reasoning 4/2022

09-01-2022

A Wos Challenge Met

Author: Robert Veroff

Published in: Journal of Automated Reasoning | Issue 4/2022

Log in

Activate our intelligent search to find suitable subject content or patents.

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.
previous article Making Higher-Order Superposition Work
next article A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
Footnotes
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.
 
Literature
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.
10.
11.
12.
13.
Metadata
Title
A Wos Challenge Met
Author
Robert Veroff
Publication date
09-01-2022
Publisher
Springer Netherlands
Published in
Journal of Automated Reasoning / Issue 4/2022
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-021-09614-y

Other articles of this Issue 4/2022

Journal of Automated Reasoning 4/2022 Go to the issue

OriginalPaper

Pardinus: A Temporal Relational Model Finder

Correction

Correction to: Local is Best: Efficient Reductions to Modal Logic K

OriginalPaper

Fast Left Kan Extensions Using the Chase

EditorialNotes

Six Decades of Automated Reasoning: Papers in Memory of Larry Wos

OriginalPaper

Faster Linear Unification Algorithm

OriginalPaper

Larry Wos: Visions of Automated Reasoning

Premium Partner

    Image Credits