Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
이 논문은 Isabelle/HOL 에서의 절차적 'apply-style' 증명 스크립트를 가독성과 견고성이 높은 선언적 Isar 증명 형식으로 자동 변환하는 'Apply2Isar' 도구를 제안하고, Isabelle 공식 증명 아카이브의 대규모 벤치마크를 통해 그 유효성을 검증합니다.
💻 Category
cs.LO
63 편의 논문
The Unit Gap: How Sharing Works in Boolean Circuits
이 논문은 AND-NOT 기저에서 부울 회로와 부울 식의 최소 크기 차이가 항상 0 또는 1 임을 증명하고, 이 차이가 1 인 경우 오직 하나의 팬아웃 2 게이트에 의한 공유 구조에서만 발생하며, 특정 변수 수 조건 하에서 공유가 불필요하거나 임계값을 갖는다는 일련의 정리들을 제시합니다.
Step Automata
이 논문은 기존 오토마타와 튜링 머신에 병렬 실행을 도입하여, 원자적 행동 단위를 수행하는 '스텝 오토마타'와 '스텝 튜링 머신 (STM)' 개념을 제안함으로써 계산과 동시성의 연결 고리를 마련합니다.
Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature
이 논문은 Lean 을 활용한 형식화를 통해 2006 년에 발표된 2HDM 잠재력 안정성 연구의 주요 정리에 오류가 있음을 발견하여, 물리학 논문에서 형식화를 통해 비자명한 오류가 처음 확인된 사례임을 보고합니다.
Central Limits via Dilated Categories
이 논문은 확률적 추론 시스템의 핵심인 중심극한정리를 위한 통일된 이론적 틀을 제공하기 위해 '확대된 반노름 enriched 범주론'을 도입하고, 이를 통해 고전적 중심극한정리 및 대수의 법칙을 일반화하고 통계역학에 적용 가능한 새로운 관측량 중심극한정리를 유도합니다.
On the expressive power of inquisitive team logic and inquisitive first-order logic
이 논문은 의문적 팀 논리 (inquisitive team logic) 의 열린 공식이 1 차 논리보다 더 높은 표현력을 가지며, 범위를 생성하는 보편 양화사를 추가하면 유한성을 표현할 수 있어 비컴팩트성과 비재귀적 공리화 가능성을 보인다는 것을 증명하고, 이를 표준 의문적 1 차 논리로 확장하여 일부 문장이 1 차 논리적이지 않은 모델 성질을 표현함을 보여줍니다.
Towards a Higher-Order Mathematical Operational Semantics
이 논문은 Turi 와 Plotkin 의 이대수적 GSOS 프레임워크를 고차 언어로 확장하여, 특정 동자연 변환인 '지시적 고차 GSOS 법칙'을 통해 고차 언어의 연산적 의미론을 정의하고 SKI 계산 및 -계산의 합성성 결과를 도출하는 이론을 제시합니다.
Consistency-based Abductive Reasoning over Perceptual Errors of Multiple Pre-trained Models in Novel Environments
이 논문은 새로운 환경에서 여러 사전 학습된 모델의 예측 오류를 식별하고 관리하기 위해 일관성 기반 귀납 추론을 적용하여, 개별 모델이나 기존 앙상블 방법보다 높은 정밀도와 재현율을 달성하는 프레임워크를 제안합니다.
A Graded Modal Type Theory for Pulse Schedules
이 논문은 양자 회로를 하드웨어 펄스 스케줄로 변환하기 위한 형식적 의미론을 제공하는 'GRAMPUS'라는 등급 모달 타입 이론을 제안하고, 이를 카테고리 이론과 초기 모델론을 통해 검증합니다.
The Skolem Problem in rings of positive characteristic
이 논문은 Dong 과 Shafrir(2026), Karimov 등 (2025) 의 최근 결과를 바탕으로 유한 생성 가환환에서의 스코렘 문제 (Skolem Problem) 가 양의 표수에서 결정 가능함을 증명하고, 해당 영집합이 Derksen(2007) 의 -정규 집합들의 유한 합집합으로 효과적으로 표현됨을 보여줍니다.
WME: Extending CDCL-based Model Enumeration with Weights
이 논문은 가중치를 고려하여 만족하는 할당 (모델) 을 나열하는 '가중치 모델 열거 (WME)' 문제를 해결하기 위해 가중치 전파, 가지치기, 충돌 분석을 CDCL 기반 알고리즘에 통합하고, 순차적 및 비순차적 백트래킹 프레임워크 간의 성능과 트레이드오프를 체계적으로 분석합니다.
A Formalization of Abstract Rewriting in Agda
이 논문은 Agda 증명 보조기를 사용하여 재귀적 추상 재작성 시스템 (ARS) 을 구성주의적으로 형식화하고, 고전 논리의 사용을 최소화하면서 종료성과 합류성에 대한 표준 결과를 정교화하고 일반화하며, 이를 람다 계산 형식화 예시를 통해 입증합니다.
Duality theory in linear optimization and its extensions -- formally verified
이 논문은 Lean 4 를 사용하여 선형 순서체에서 파카스 (Farkas) 와 유사한 정리들을 형식적으로 증명하고, 일부 계수가 '무한대' 값을 가질 수 있는 경우로 선형 최적화의 쌍대성 이론을 확장합니다.
Constraint satisfaction problems, compactness and non-measurable sets
이 논문은 유한 관계 구조 A 의 폭이 1 일 때 ZFC 공리계 내에서 A 의 콤팩트성이 증명되지만, 그렇지 않은 경우에는 3 차원 공간에서 비가측 집합의 존재를 함의함을 보여줍니다.
A Topological Rewriting of Tarski's Mereogeometry
이 논문은 의존형 타입 이론과 Coq 증명 보조기를 기반으로 람다-MM 라이브러리를 확장하여 타르스키의 기하학을 단순한 질적 공간 모델이 아닌 위상 공간으로 재구성하고, 그 위상적 성질을 증명함으로써 이론의 표현력을 강화합니다.
Can LLM Aid in Solving Constraints with Inductive Definitions?
이 논문은 대규모 언어 모델 (LLM) 이 유도적 정의와 관련된 제약 조건을 해결하는 데 필요한 보조 명제를 생성하고, 이를 제약 해결기와 결합한 신경-심볼릭 접근법을 통해 기존 솔버의 성능을 약 25% 향상시켰음을 보여줍니다.
Model Change for Description Logic Concepts
이 논문은 설명 논리 (Description Logic) 개념을 모델 (지시된 해석) 에 기반하여 수정하는 '모델 변경' 문제를 다루며, 배제, 수용, 수정이라는 세 가지 유형을 정의하고, 특히 수정이 배제와 수용의 단순한 조합으로 환원되지 않음을 증명하며 EL 및 ALC 논리 체계에서의 호환성에 대한 긍정적 및 부정적 결과를 제시합니다.
Classical Explanations in (and of) General Probabilistic Theories
이 논문은 확률 모델 간의 '설명'을 범주론적 스팬으로 정의하고, 이를 통해 모든 국소 유한 확률 이론이 표준적인 고전적 설명을 갖는다는 것을 보임으로써, 일반 확률 이론에 대한 범주론적 해석을 제시합니다.
LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning
이 논문은 제한된 자원 환경의 소형 언어 모델이 자연어 요구사항으로부터 일관된 선형 시간 논리 (LTL) 명세를 생성할 수 있도록, 제약 생성과 경량 형식 검증 도구를 결합한 모듈형 도구체인 'LTLGuard'를 제안합니다.
Diagonalizing Through the -Chain: Iterated Self-Certification on Bounded Turing Machines and its Least Fixed Point
이 논문은 유계 튜링 기계의 자기 인증이 시간 오버헤드로 인해 실패하지만, 이 과정을 도메인 이론의 -체인으로 확장하여 스콧 극한을 취함으로써 유한 관측에서 무한 계산의 최소 고정점으로의 전이를 설명하고 정지 문제를 새로운 관점에서 해석함을 보여줍니다.