Skip to main content
main-content

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

25.02.2020 | Ausgabe 3/2020

Journal of Automated Reasoning 3/2020

SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment

Zeitschrift:
Journal of Automated Reasoning > Ausgabe 3/2020
Autoren:
Andreas Teucke, Christoph Weidenbach
Wichtige Hinweise

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Abstract

We introduce FO-AR, an approximation-refinement approach for first-order theorem proving based on counterexample-guided abstraction refinement. A given first-order clause set N is transformed into an over-approximation \(N^{\prime }\) in a decidable first-order fragment. That means if \(N^{\prime }\) is satisfiable so is N. However, if \(N^{\prime }\) is unsatisfiable, then the approximation provides a lifting terminology for the found refutation which is step-wise transformed into a proof of unsatisfiability for N. If this fails, the cause is analyzed to refine the original clause set such that the found refutation is ruled out for the future and the procedure repeats. The target fragment of the transformation is the monadic shallow linear fragment with straight dismatching constraints, which we prove to be decidable via ordered resolution with selection. We further discuss practical aspects of SPASS-AR, a first-order theorem prover implementing FO-AR. We focus in particularly on effective algorithms for lifting and refinement.

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

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 + Umwelt
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Testen Sie jetzt 30 Tage kostenlos.

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




Testen Sie jetzt 30 Tage kostenlos.

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 + Umwelt
  • Maschinenbau + Werkstoffe




Testen Sie jetzt 30 Tage kostenlos.

Literatur
Über diesen Artikel

Weitere Artikel der Ausgabe 3/2020

Journal of Automated Reasoning 3/2020 Zur Ausgabe

Premium Partner

    Bildnachweise