63 Arbeiten
Die Arbeit stellt Apply2Isar vor, ein Werkzeug für Isabelle/HOL, das automatisch prozedurale „Apply-Style"-Beweisskripte in lesbare und robuste deklarativen Isar-Beweise umwandelt, wie eine Auswertung auf Basis des Isabelle Archive of Formal Proofs zeigt.
Die Arbeit beweist, dass die Lücke zwischen der minimalen Größe einer Booleschen Schaltung und einer Booleschen Formel über dem AIG-Basis immer 0 oder 1 beträgt, wobei ein Wert von 1 ausschließlich durch eine einzige Gatterteilung mit Fan-out 2 entsteht, sobald die Anzahl der essentiellen Variablen einen bestimmten Schwellenwert überschreitet.
Der Artikel führt die Konzepte des Schrittautomaten und der Schrittmaschine (STM) ein, um als natürliche Erweiterung traditioneller Automaten und der klassischen Turingmaschine eine Lücke in der Verbindung von Berechnungstheorie und Nebenläufigkeit zu schließen, indem er die Ausführung von atomaren Aktionsschritten ohne partielle Ordnungen ermöglicht.
Diese Arbeit dokumentiert, wie die Formalisierung des 2HDM-Potentials in Lean einen Fehler in der weit verbreiteten Stabilitätsanalyse von Maniatis et al. (2006) aufdeckte und damit erstmals einen nicht-trivialen Irrtum in der Physikliteratur durch interaktive Theorembeweiser identifiziert.
Diese Arbeit stellt die dilatierte seminormen-angereicherte Kategorientheorie als vereinheitlichendes Rahmenwerk für zentrale Grenzwertsätze vor, in dem ein abstrakter zentraler Grenzwertsatz bewiesen wird, der sowohl klassische Ergebnisse wie das Gesetz der großen Zahlen als auch neue Sätze für symplektische Mannigfaltigkeiten umfasst.
Die Arbeit zeigt, dass die Ausdruckskraft offener Formeln der inquisitiven Teamlogik und bestimmter Sätze der inquisitiven Prädikatenlogik die der klassischen Prädikatenlogik erster Stufe übersteigt, wobei erstere sogar die Endlichkeit ausdrücken kann, was zu mangelnder Kompaktheit und Nichtrekursiver Axiomatisierbarkeit führt.
Dieser Artikel entwickelt eine Theorie abstrakter GSOS-Spezifikationen für höherstufige Sprachen, die das Bialgebra-Framework von Turi und Plotkin auf diesen Bereich überträgt und durch die Einführung von „pointed higher-order GSOS laws" allgemeine Kompositionalitätsresultate für Systeme wie den SKI-Kalkül und den λ-Kalkül liefert.
Diese Arbeit stellt einen konsistenzbasierten abduktiven Rahmen vor, der durch die logische Integration und Fehlerfilterung mehrerer vortrainierter Wahrnehmungsmodelle deren Leistung in neuen Umgebungen mit Verteilungsverschiebungen signifikant verbessert.
Dieses Paper stellt GRAMPUS vor, eine neuartige Sprache auf Basis einer abgestuften modalen Typtheorie, die es ermöglicht, Quantenschaltkreise für supraleitende Qubits formal semantisch präzise in zeitlich spezifizierte Mikrowellen-Impulspläne zu übersetzen.
Die Autoren zeigen, dass das Skolem-Problem in endlich erzeugten kommutativen Ringen positiver Charakteristik entscheidbar ist, indem sie neuere Ergebnisse zu S-Einheiten-Gleichungen und linearen Gleichungen über multiplikativ unabhängigen Zahlen nutzen, um nachzuweisen, dass die Nullstellenmenge einer linearen Rekurrenzfolge effektiv als endliche Vereinigung von -normalen Mengen dargestellt werden kann.
Diese Arbeit stellt CDCL-basierte Algorithmen für die gewichtete Modellenumeration (WME) vor, die Gewichtspropagation und -pruning integrieren, um gewichtsbasierte Abfragen wie Top-k-Modelle effizient zu lösen, und vergleicht dabei chronologische und nicht-chronologische Backtracking-Ansätze hinsichtlich ihrer jeweiligen Stärken und Kompromisse.
Dieses Papier stellt eine konstruktive Formalisierung von Abstrakten Umformungssystemen in Agda vor, die klassische Logik eliminiert, Terminierteits- und Konfluenzbeziehungen untersucht und die Anwendbarkeit durch eine Lambda-Kalkül-Formalisierung demonstriert.
Dieses Papier stellt in Lean 4 formal verifizierte Farkas-artige Sätze über linear geordneten Körpern vor und erweitert die Dualitätstheorie der linearen Optimierung auf den Fall, dass einige Koeffizienten unendliche Werte annehmen dürfen.
Die Arbeit zeigt, dass die Kompaktheit endlicher relationaler Strukturen mit Breite eins bereits in ZFC beweisbar ist, während sie im Allgemeinen die Existenz nicht-messbarer Mengen im dreidimensionalen Raum impliziert.
Dieser Beitrag erweitert eine formale Mereologie in Coq um eine topologische Struktur, die Tarskis Geometrie als Unterraum integriert, indem er zeigt, dass mereologische Klassen regulären offenen Mengen entsprechen und damit eine ausdrucksstärkere, hausdorffsche geometrische Theorie ermöglicht.
Die vorgestellte Arbeit demonstriert, dass ein neuro-symbolischer Ansatz, der Large Language Models zur Generierung von Hilfslemmata mit Constraint-Lösern kombiniert, die Erfolgsrate beim Lösen von Induktionsdefinitionen um etwa 25 % gegenüber dem aktuellen Stand der Technik steigert.
Die Arbeit untersucht das Problem der Modelländerung für Beschreibungslogikkonzepte, indem sie die Operationen Eviction, Reception und Revision formal definiert und die Kompatibilität dieser Ansätze für die Logiken EL und ALC analysiert, wobei gezeigt wird, dass Revision nicht einfach als Kombination von Eviction und Reception aufgefasst werden kann.
Die Arbeit führt den Begriff der Erklärung probabilistischer Modelle als spezielle Spanne in der Kategorie ein, zeigt die Kompositionsfähigkeit dieser Erklärungen und beweist, dass jedes lokal-endliche probabilistische Modell eine kanonische, scharfe klassische Darstellung besitzt.
Das Paper stellt LTLGuard vor, ein modulares Werkzeug, das kompakte Sprachmodelle mit formalen Konsistenzprüfungen kombiniert, um aus unpräzisen natürlichen Sprachanforderungen korrekte und widerspruchsfreie LTL-Spezifikationen zu generieren.
Die Arbeit zeigt, dass die Selbstzertifizierung auf beschränkten Turingmaschinen zwar aufgrund zeitlicher Überhauung nicht zu einem Fixpunkt führt, aber durch die Scott-Grenze einer aufsteigenden -Kette dennoch einen unbeschränkten Fixpunkt liefert, der das vollständige Halteverhalten erfasst.