h1

h2

h3

h4

h5
h6

DFG project G:(GEPRIS)531314152

SMT Techniken für arithmetische Theorien

CoordinatorProfessorin Dr. Erika Ábrahám
Grant period2024 -
Funding bodyDeutsche Forschungsgemeinschaft
 DFG
IdentifierG:(GEPRIS)531314152

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.
   

Recent Publications

All known publications ...
Download: BibTeX | EndNote XML,  Text | RIS | 

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Contribution to a book/Contribution to a conference proceedings  ;  ;  ;  ;  ;  ;  ;
Projective Delineability for Single Cell Construction
SC-Square 2025 : Satisfiability Checking and Symbolic Computation 2025 : Proceedings of the 10th International Workshop on Satisfiability Checking and Symbolic Computation (SC-Square 2025), Collocated with The 30th International Conference on Automated Deduction (CADE 2025) : Stuttgart, Germany, August 2, 2025 / Edited by Mădălina Erașcu, Mikoláš Janota
10. International Workshop on Satisfiability Checking and Symbolic Computation, SC-Square 2025, StuttgartStuttgart, Germany, 2 Aug 2025 - 2 Aug 20252025-08-022025-08-02
30. International Conference on Automated Deduction, CADE 2025, StuttgartStuttgart, Germany, 28 Jul 2025 - 2 Aug 20252025-07-282025-08-02 Aachen, Germany : RWTH Aachen, CEUR workshop proceedings 4116, 41-54 () [10.18154/RWTH-2025-10263]  GO OpenAccess  Download fulltext Files  Download fulltextHomepage of book Download fulltextFulltext BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Contribution to a book/Contribution to a conference proceedings  ;
A Variant of Non-uniform Cylindrical Algebraic Decomposition for Real Quantifier Elimination
SC-Square 2025 : Satisfiability Checking and Symbolic Computation 2025 : Proceedings of the 10th International Workshop on Satisfiability Checking and Symbolic Computation (SC-Square 2025), Collocated with The 30th International Conference on Automated Deduction (CADE 2025) : Stuttgart, Germany, August 2, 2025 / Edited by Mădălina Erașcu, Mikoláš Janota
10. International Workshop on Satisfiability Checking and Symbolic Computation, SC-Square 2025, StuttgartStuttgart, Germany, 2 Aug 2025 - 2 Aug 20252025-08-022025-08-02
30. International Conference on Automated Deduction, CADE 2025, StuttgartStuttgart, Germany, 28 Jul 2025 - 2 Aug 20252025-07-282025-08-02 Aachen, Germany : RWTH Aachen, CEUR workshop proceedings 4116, 19-34 () [10.18154/RWTH-2025-10262]  GO OpenAccess  Download fulltext Files  Download fulltextHomepage of book Download fulltextFulltext BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Journal Article  ;  ;  ;
FMplex: Exploring a Bridge between Fourier-Motzkin and Simplex
Logical methods in computer science : LMCS 21(2), 13362 () [10.46298/lmcs-21(2:6)2025]  GO OpenAccess  Download fulltext Files BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Contribution to a book/Contribution to a conference proceedings  ;  ;  ;  ;  ;  ;  ;
On Projective Delineability
2024 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-19 Pisctaway, NJ : IEEE 9-16 () [10.1109/SYNASC65383.2024.00015]  GO BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Abstract (Extended abstract)/Contribution to a book/Contribution to a conference proceedings  ;  ;
Under-Approximation of a Single Algebraic Cell
PAAR+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-02 Aachen, Germany : RWTH Aachen, CEUR workshop proceedings 3717, 132-136 ()  GO   Download fulltextHomepage of book Download fulltextFulltext BibTeX | EndNote: XML, Text | RIS

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Contribution to a book/Contribution to a conference proceedings  ;
Merging Adjacent Cells During Single Cell Construction
Computer 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-06 Cham, Switzerland : Springer, Lecture notes in computer science 14938, 252-272 () [10.1007/978-3-031-69070-9_15]  GO BibTeX | EndNote: XML, Text | RIS

All known publications ...
Download: BibTeX | EndNote XML,  Text | RIS | 

 Record created 2024-02-19, last modified 2024-09-26
Similar records



Rate this document:

Rate this document:
1
2
3
4
5
 
(Not yet reviewed)