64 papers
Dit artikel introduceert Apply2Isar, een tool die automatisch procedurele 'apply-style' bewijzen in Isabelle/HOL converteert naar leesbare en robuuste declaratieve Isar-bewijzen, en de effectiviteit ervan valideert met bewijzen uit het Isabelle Archive of Formal Proofs.
Dit artikel bewijst dat het verschil tussen de minimale grootte van een Boolese schakeling en een formule in de AIG-basis altijd 0 of 1 is, en dat delen van subexpressies alleen nodig is wanneer het aantal essentiële variabelen een bepaalde drempel overschrijdt.
In dit paper introduceren de auteurs het concept van stapautomata en stap-Turingmachines als een natuurlijke uitbreiding van traditionele automata en Turingmachines die het uitvoeren van een stap van atomaire acties mogelijk maakt zonder partiële ordening.
Dit artikel beschrijft hoe formalisatie in Lean een fout heeft blootgelegd in een veel geciteerde 2006-publicatie over de stabiliteit van het twee-Higgs-dubbelletmodel, wat het eerste geval is van een niet-triviale fout in de natuurkunde die via deze methode is ontdekt.
Dit paper introduceert dilated seminorm-enriched categorietheorie als een unificerend raamwerk voor centrale limieten, waarmee een abstracte centrale limietstelling wordt bewezen die zowel klassieke resultaten als een nieuwe stelling voor symplectische variëteiten omvat.
Dit artikel toont aan dat de uitdrukkingskracht van open formules in inquisitieve teamlogica en inquisitieve eerste-orde logica strikt groter is dan die van de eerste-orde logica, en dat een uitbreiding met een universele kwantificator die een bereik genereert, de mogelijkheid biedt om eindigheid uit te drukken, wat leidt tot het ontbreken van compactheid en recursieve axiomatiseerbaarheid.
Deze paper ontwikkelt een theorie van abstracte GSOS-specificaties voor hogere-orde talen die compositionaliteitsbewijzen mogelijk maakt door het Turi-Plotkin-raamwerk uit te breiden naar een hogere-orde setting, waarbij de operationele semantiek wordt weergegeven als gepunte hogere-orde GSOS-wetten.
Dit artikel introduceert een consistentie-gebaseerde abductieve redeneerframework dat testtijd-logische regels en meerdere pre-getrainde modellen combineert om prestatieverlies door distributieverschuivingen in nieuwe omgevingen effectief te mitigeren en zo zowel de precisie als het recall significant te verbeteren.
Dit paper introduceert GRAMPUS, een getypeerde modale theorie met graden die tijdsinformatie coderen, als een formeel taalmodel voor het specificeren en analyseren van microgolf-pulsschema's voor supergeleidende quantumcomputers.
Dit artikel bewijst dat het Skolem-probleem voor lineaire recurrente rijen in eindig gegenereerde commutatieve ringen van positieve karakteristiek beslisbaar is, door gebruik te maken van recente resultaten over S-eenheidvergelijkingen en lineaire vergelijkingen.
Dit paper introduceert Weighted Model Enumeration (WME) als een nieuwe solver-taak en presenteert CDCL-gebaseerde algoritmen die gewichtsinformatie integreren in zowel chronologische als niet-chronologische backtracking-frames voor het efficiënt enumereren van modellen op basis van hun gewichten.
Dit artikel presenteert een constructieve formalisatie van abstracte herschrijvingssystemen in Agda, waarbij klassieke logica wordt geëlimineerd, relaties tussen terminatie- en confluëntiebegrippen worden onderzocht, en de toepasbaarheid wordt geïllustreerd aan de hand van de lambda-calculus.
Dit paper presenteert een formeel geverifieerde implementatie in Lean 4 van diverse Farkas-achtige stellingen over lineair geordende velden en breidt de dualiteitstheorie uit naar het geval waarin sommige coëfficiënten oneindige waarden mogen aannemen.
Het artikel toont aan dat de compactheid van een eindige relationele structuur A binnen ZFC bewezen kan worden als A breedte één heeft, terwijl compactheid anders de existentie van niet-meetbare verzamelingen in de driedimensionale ruimte impliceert.
Dit artikel presenteert een topologische herschrijving van Tarski's mereogeometrie binnen de Coq-omgeving, waarbij een algebraïsche formulering van topologische relaties wordt gebruikt om een volledige topologische ruimte af te leiden uit mereologie en Tarski's axioma's te reduceren en uit te breiden met de Hausdorff-eigenschap.
Dit paper introduceert een neuro-symbolische aanpak die Large Language Models combineert met constraint-solvers om via gegenereerde lemmata het oplossen van beperkingen met inductieve definities aanzienlijk te verbeteren.
Dit artikel introduceert een formeel kader voor het wijzigen van beschrijvingslogica-concepten door middel van evictie, receptie en revisie, en toont aan dat revisie niet eenvoudigweg als een combinatie van de eerste twee kan worden opgevat, terwijl het ook resultaten presenteert over de compatibiliteit van deze operaties voor EL en ALC.
Dit artikel introduceert een categorische definitie van "verklaring" tussen probabilistische modellen en toont aan dat elke lokaal-finite probabilistische theorie een canonieke, scherpe klassieke representatie bezit die funtoriëel wordt geconstrueerd via pullbacks.
Dit paper introduceert LTLGuard, een modulaire toolchain die compacte taalmodellen combineert met lichtgewicht symbolische redeneertools om uit informele eisen correcte en consistentie Linear Temporal Logic (LTL)-specificaties te genereren.
Dit paper toont aan dat hoewel zelfverificatie binnen een Turingmachine door tijdsvertraging geen vast punt bereikt, de iteratieve constructie via een -keten wel convergeert naar een Scott-limiet die het halteringsprobleem als een continu uitgestelde diagonaal oplost.