Note: Der Einsatz von Computern zum Lösen industriell relevanter Probleme ist schon lange etabliert. Eine aktuelle Entwicklung ermöglicht es, Probleme als logische Formeln erster Ordnung zu kodieren und diese automatisiert zu Lösen. SAT- und SMT-Solver (Satisfiability Modulo Theories) bieten hierzu Werkzeuge zur Überprüfung der Erfüllbarkeit dieser Formeln. SAT-Solver unterstützen Aussagenlogik, während SMT-Solver verschiedene Theorien beherrschen. Arithmetische Theorien sind im Fokus dieses Antrags und sind in diversen SMT-Solvern implementiert, darunter SMT-RAT, entwickelt von der RWTH, und veriT von der ULiège. Erfüllbarkeitsüberprüfung ist ein junges und sich schnell entwickelndes Forschungsgebiet. Es gibt sehr effiziente Solver für eine Menge von Theorien, einschließlich (quantorenfreier) linearer reeller, ganzzahliger und gemischt ganzzahlig-realer Arithmetik (LRA, LIA bzw. LIRA), d.h. für Formeln, die boolesche Kombinationen von linearen Bedingungen sind. Die Erweiterung um die Multiplikation ergibt die entsprechenden nichtlinearen arithmetischen Theorien NRA, NIA und NIRA, wobei die beiden letzteren im quantorenfreien Fall unentscheidbar sind. SMT-Techniken für lineare Arithmetik sind ausgereift, auch wenn es noch einige unerforschte, aber interessante Aspekte gibt, die wir in diesem Antrag adressieren. Im Gegensatz zum linearen Fall und trotz vielversprechender Entwicklungen sind die derzeitigen Algorithmen für NRA noch nicht zufriedenstellend. Ziel dieses Antrags ist die Verbesserung bestehender und die Entwicklung neuer Algorithmen für arithmetische Theorien. Bei der nichtlinearen Arithmetik konzentrieren wir uns aufgrund der Unentscheidbarkeit des ganzzahligen Falls hauptsächlich auf den reellen Fall. SMT-Solver werden auch in Bereichen eingesetzt, wo die Korrektheit der Antworten unerlässlich ist, z.B. zur Verifikation, in Beweis-Assistenten oder in der erklärbaren KI. Jüngste Entwicklungen erweitern SMT-Solver, sodass diese nicht nur Modelle für erfüllbare Probleme liefern, sondern auch Beweise für Unerfüllbarkeit, die extern verifiziert werden können. Allerdings wird dies für die Arithmetik noch nicht vollständig unterstützt. In diesem Projekt wollen wir das Konzept der Zertifikate und Modelle für die lineare Arithmetik konsolidieren und den Weg für Zertifikate für die nichtlineare Arithmetik ebnen. Trotz der jahrelangen Erforschung auch im Bereich der mathematischen Logik und symbolischen Rechnen sind verschiedene Aspekte der Algorithmen für Arithmetik noch nicht vollständig verstanden. Es gibt weiteren Forschungsbedarf zum Verständnis der Komplexität. So gibt es zum Beispiel nur eine vollständige Methode für LRA-Bedingungen mit polynomialem Aufwand, und es gibt immer noch keine Methode, die die einfach-exponentielle Komplexitätsgrenze für NRA implementiert. Ein weiteres Ziel ist es, ein tieferes Verständnis für die Natur der arithmetischen Probleme, ihrer Komplexität und die Struktur ihrer Lösungsmengen zu schaffen.
http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.pngContribution to a book/Contribution to a conference proceedingsMichel, L. (Corresponding author) ; Nalbach, J. K. F.RWTH* ; Mathonet, P. ; Zénaïdi, N. ; Brown, C. W. ; Ábrahám, E.RWTH* ; Davenport, J. H. ; England, M. On Projective Delineability 20242024 26th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC) : [Proceedings] 26. International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2024, TimisoaraTimisoara, Romania, 16 Sep 2024 - 19 Sep 20242024-09-162024-09-19Pisctaway, NJ : IEEE9-16(2024)[10.1109/SYNASC65383.2024.00015]2024BibTeX |
EndNote:
XML,
Text |
RIS
http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.pngAbstract (Extended abstract)/Contribution to a book/Contribution to a conference proceedingsPromies, V. M. (Corresponding author)RWTH* ; Nalbach, J. K. F.RWTH* ; Ábrahám, E.RWTH* Under-Approximation of a Single Algebraic Cell 2024PAAR+SC-Square 2024: Practical Aspects of Automated Reasoning and Satisfiability Checking and Symbolic Computation Workshop 2024 : joint proceedings of the 9th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 9th Satisfiability Checking and Symbolic Computation Workshop (SC-Square), 2024, co-located with the 12th International Joint Conference on Automated Reasoning (IJCAR 2024) : Nancy, France, July 2, 2024 / edited by Chris Brown, Daniela Kaufmann, Cláudia Nalon, Alexander Steen, Martin Suda 9. Workshop on Practical Aspects of Automated Reasoning, PAAR 2024, NancyNancy, France, 2 Jul 2024 - 2 Jul 20242024-07-022024-07-02 12. International Joint Conference on Automated Reasoning, IJCAR 2024, NancyNancy, France, 2 Jul 2024 - 2 Jul 20242024-07-022024-07-02 9. Satisfiability Checking and Symbolic Computation Workshop, SC-Square 2024, NancyNancy, France, 2 Jul 2024 - 2 Jul 20242024-07-022024-07-02Aachen, Germany : RWTH Aachen, CEUR workshop proceedings3717,132-136(2024)2024Homepage of bookFulltextBibTeX |
EndNote:
XML,
Text |
RIS
http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.pngContribution to a book/Contribution to a conference proceedingsNalbach, J. K. F. (Corresponding author)RWTH* ; Ábrahám, E.RWTH* Merging Adjacent Cells During Single Cell Construction 2024Computer algebra in scientific computing : 26th international workshop, CASC 2024, Rennes, France, September 2-6, 2024 : proceedings / François Boulier, Chenqi Mou, Timur M. Sadykov, Evgenii V. Vorozhtsov, editors 25. International Workshop on Computer Algebra in Scientific Computing, CASC 2024, RennesRennes, France, 2 Sep 2024 - 6 Sep 20242024-09-022024-09-06Cham, Switzerland : Springer, Lecture notes in computer science14938,252-272(2024)[10.1007/978-3-031-69070-9_15]2024BibTeX |
EndNote:
XML,
Text |
RIS
guest ::
Files
BibTeX |
EndNote:
XML,
Text |
RIS