64 articles
L'article présente Apply2Isar, un outil qui convertit automatiquement les scripts de preuve procéduraux de style « apply » en Isabelle/HOL en preuves déclaratives structurées Isar, alliant ainsi la rapidité d'exploration de la première méthode à la lisibilité et la robustesse de la seconde.
Ce papier démontre que l'écart entre la taille minimale d'un circuit booléen et celle d'une formule sur la base AIG est toujours 0 ou 1, caractérisant précisément les conditions d'optimisation et les structures de partage nécessaires pour atteindre cette borne.
Cet article propose les concepts d'automate à étapes et de machine de Turing à étapes (STM) comme extensions naturelles des modèles classiques, permettant l'exécution d'actions atomiques pour combler le lien manquant entre la machine de Turing et l'automate concurrent.
En formalisant la preuve de stabilité du potentiel du modèle à deux doublets de Higgs dans l'assistant de preuves Lean, les auteurs ont découvert une erreur invalidant le théorème principal d'un article de référence de 2006, marquant ainsi la première détection d'une telle erreur non triviale dans la littérature physique grâce à cette méthode.
Cet article introduit la théorie des catégories enrichies en semi-normes dilatées comme cadre unificateur pour établir un théorème central limite abstrait, permettant de dériver des résultats classiques ainsi qu'un nouveau théorème pour les variétés symplectiques applicable à la mécanique statistique.
Cet article démontre que la logique d'équipe inquisitive, bien que équivalente à la logique du premier ordre pour les phrases, possède une puissance expressive supérieure pour les formules ouvertes, et que son extension avec un quantificateur universel générant des domaines permet d'exprimer la finitude, rendant ainsi la logique non compacte et non axiomatisable.
Cet article développe une théorie des spécifications GSOS abstraites pour les langages d'ordre supérieur, en introduisant des lois GSOS pointées sous forme de transformations dinaturelles qui garantissent la compositionnalité de la sémantique opérationnelle, comme l'illustrent les calculs SKI et .
Cet article propose un cadre d'abduction basé sur la cohérence qui intègre les prédictions de multiples modèles pré-entraînés via des règles logiques pour atténuer les erreurs de perception dans des environnements nouveaux, surpassant ainsi les modèles individuels et les méthodes d'ensemble classiques en termes de précision et de rappel.
Cet article propose GRAMPUS, une théorie des types modaux gradués qui utilise des grades temporels pour formaliser sémantiquement et catégoriellement les séquences de signaux de contrôle (pulse schedules) nécessaires à l'exécution des circuits quantiques sur des qubits supraconducteurs.
Cet article démontre que le problème de Skolem est décidable dans les anneaux commutatifs de type fini de caractéristique positive, en établissant que l'ensemble des zéros d'une suite récurrente linéaire sur un tel anneau est une union finie effective d'ensembles -normaux.
Cet article présente des algorithmes basés sur CDCL pour l'énumération de modèles pondérés (WME), une tâche de résolution qui intègre la propagation, l'élagage et l'analyse de conflits pondérés dans des cadres de retour en arrière chronologiques et non chronologiques pour permettre des requêtes guidées par les poids.
Cet article présente une formalisation constructive des systèmes de réécriture abstraits dans l'assistant de preuve Agda, visant à éliminer l'usage de la logique classique, à affiner les critères de terminaison et de confluence, et à illustrer cette approche par une formalisation du lambda-calcul.
Cet article présente la formalisation en Lean 4 de plusieurs théorèmes de type Farkas sur les corps ordonnés et l'extension de la théorie de la dualité en optimisation linéaire aux coefficients infinis.
Cet article démontre que la compacité d'une structure relationnelle finie de largeur un est prouvable dans ZF, tandis que la compacité d'une structure de largeur supérieure implique l'existence d'ensembles non mesurables dans l'espace à trois dimensions.
Cet article présente une reformulation topologique de la géométrie de Tarski en étendant la bibliothèque lambda-MM sous Coq pour établir une correspondance entre les classes méreologiques et les ensembles ouverts réguliers, permettant ainsi de dériver un espace topologique complet et d'ajouter des propriétés géométriques comme l'axiome de séparation T2.
Cet article propose une approche neuro-symbolique combinant les grands modèles de langage et les solveurs de contraintes pour générer itérativement des lemmes auxiliaires, améliorant ainsi de manière significative la résolution des contraintes impliquant des définitions inductives par rapport aux méthodes actuelles.
Cet article introduit le concept de « changement de modèle » pour les concepts de logique de description, en distinguant l'éviction, la réception et la révision, et en démontrant que la révision ne se réduit pas à une simple combinaison des deux premières opérations, tout en présentant des résultats sur leur compatibilité dans les logiques EL et ALC.
Cet article introduit une notion d'explication de modèles probabilistes généralisés via des spans dans la catégorie , démontrant que ces explications se composent et que tout modèle probabiliste localement fini admet une explication classique canonique et précise, fournissant ainsi une représentation classique functorielle pour toute théorie probabiliste localement finie.
LTLGuard est un outil modulaire qui combine la génération contrainte et la vérification formelle pour permettre aux modèles de langage compacts (4B–14B paramètres) de transformer des exigences informelles en spécifications LTL correctes et cohérentes.
En traduisant l'échec de l'autocertification bornée des machines de Turing en un cadre théorique des domaines, cet article démontre que la limite de Scott d'une chaîne croissante d'observations finies converge vers un point fixe minimal correspondant à un calcul illimité qui résout le problème de l'arrêt.