63 articoli
Il paper introduce Apply2Isar, uno strumento per Isabelle/HOL che converte automaticamente script di prova procedurali in stile "apply" in dimostrazioni dichiarative Isar, migliorando così la leggibilità e la robustezza dei codici esistenti.
Il documento dimostra che il divario tra la dimensione minima di un circuito booleano e quella di una formula è sempre 0 o 1, stabilendo che tale differenza unitaria deriva esclusivamente da un singolo gate con fan-out pari a 2 e fornendo condizioni precise su quando la condivisione delle sottoreti è necessaria.
Il documento propone i concetti di automa a passo e macchina di Turing a passo (STM) come estensioni naturali degli automi e delle macchine di Turing tradizionali che permettono l'esecuzione di un singolo passo di azioni atomiche, colmando così la lacuna esistente nella letteratura tra la macchina di Turing e gli automi concorrenti.
Questo articolo descrive come la formalizzazione in Lean del lavoro del 2006 sulla stabilità del potenziale del modello a due doppietti di Higgs abbia rivelato un errore fondamentale negli argomenti originali, segnando la prima scoperta di un errore non banale in un articolo di fisica ottenuta tramite tale metodo.
Questo articolo introduce la teoria delle categorie seminormate dilatate come quadro unificante per il Teorema del Limite Centrale, permettendo di derivare sia risultati classici rafforzati che un nuovo teorema applicabile alle varietà simplettiche nella meccanica statistica.
Il documento dimostra che, sebbene la logica inquisitiva di squadra sia equivalente alla logica del primo ordine per le frasi, i suoi aperti possiedono un potere espressivo superiore, permettendo di esprimere proprietà non definibili in logica del primo ordine e, se estesa con un quantificatore universale specifico, di definire la finitezza, rendendola non compatta e non assiomatizzabile.
Questo lavoro sviluppa una teoria delle specifiche GSOS astratte per i linguaggi di ordine superiore, trasferendo i principi del quadro di Turi e Plotkin a tale contesto mediante trasformazioni dinaturali chiamate leggi GSOS di ordine superiore puntate, al fine di garantire risultati generali di composizionalità che si applicano, tra gli altri, al calcolo SKI e al -calcolo.
Questo paper propone un quadro di ragionamento abduttivo basato sulla coerenza che integra le previsioni di modelli pre-addestrati multipli in ambienti nuovi, utilizzando regole logiche per identificare e gestire errori percettivi, ottenendo così miglioramenti significativi nella precisione e nel richiamo rispetto ai singoli modelli e alle basi di ensemble standard.
Il paper propone GRAMPUS, una teoria dei tipi modale graduata che utilizza i gradi per rappresentare le informazioni temporali, al fine di fornire un linguaggio formalmente semantico per la specifica degli impulsi di controllo nei computer quantistici a qubit superconduttori.
Il paper dimostra che il Problema di Skolem è decidibile negli anelli commutativi finitamente generati di caratteristica positiva, fornendo un algoritmo che determina se una successione di ricorrenza lineare su tali anelli contiene un termine nullo.
Questo lavoro introduce e analizza algoritmi basati su CDCL per l'Enumerazione di Modelli Ponderati (WME), integrando la propagazione e il pruning dei pesi per abilitare query guidate dai pesi e confrontando l'efficacia delle strategie di backtracking cronologico e non cronologico.
Il paper presenta una formalizzazione costruttiva dei sistemi di riscrittura astratti in Agda, eliminando la logica classica per affinare i criteri di terminazione e confluenza e dimostrandone l'applicabilità attraverso un esempio nel calcolo lambda.
Questo articolo presenta la formalizzazione in Lean 4 di diversi teoremi simili a quello di Farkas su campi ordinati linearmente e estende la teoria della dualità nell'ottimizzazione lineare per includere coefficienti che possono assumere valori infiniti.
Il documento dimostra che la compattezza di una struttura relazionale finita è dimostrabile in ZF se la struttura ha larghezza uno, mentre altrimenti la sua validità implica l'esistenza di insiemi non misurabili nello spazio tridimensionale.
Questo articolo presenta una riscrittura topologica della geometria di Tarski, implementata nel proof assistant Coq tramite la libreria lambda-MM, che estende il mereologia di Lesniewski per derivare uno spazio topologico completo e dimostrare che le classi mereologiche corrispondono a insiemi aperti regolari, riducendo così il sistema assiomatico originale e arricchendolo con proprietà come quella di Hausdorff.
Questo lavoro propone un approccio neuro-simbolico che integra i Large Language Models con i solutori di vincoli per generare iterativamente lemma ausiliari, migliorando significativamente la capacità di risolvere vincoli contenenti definizioni induttive rispetto agli strumenti esistenti.
Il paper introduce il concetto di "model change" per le logiche descrittive, distinguendo tra evizione, ricezione e revisione, e analizza i risultati teorici sulla loro compatibilità e sulla natura non riducibile della revisione nelle logiche EL e ALC.
Il paper introduce una nozione di "spiegazione" tra modelli probabilistici generalizzati come un particolare tipo di span nella categoria , dimostrando che tali spiegazioni si compongono tramite pullback e che ogni modello probabilisticamente localmente finito ammette una spiegazione classica canonica e precisa, la cui costruzione è funtoriale.
Il paper presenta LTLGuard, un approccio modulare che combina la generazione di modelli linguistici compatti con la verifica simbolica formale per tradurre in modo efficiente e affidabile requisiti informali in specifiche corrette in logica temporale lineare (LTL).
Il documento dimostra che, sebbene l'autocertificazione limitata nelle macchine di Turing fallisca a causa di un sovraccarico temporale, il processo iterativo attraverso una catena converge al limite di Scott, definendo un punto fisso minimo che rappresenta un calcolo illimitato capace di catturare completamente il comportamento di arresto.