Journal of Automated Reasoning

Journal of Automated Reasoning（常用缩写 J. Autom. Reason.，CODEN 为 JAREEW）是逻辑推理自动化领域的同行评审学术期刊，由施普林格（Springer）以混合获取模式出版，每年 8 期。该刊创刊于 1983 年，由 Larry Wos 创办并担任首任主编（至 1992 年）。Journal of Automated Reasoning (commonly abbreviated as ''J. Autom. Reason.', CODEN JAREEW) is a peer-reviewed journal dedicated to automated reasoning, published by Springer under a hybrid model with eight issues per year. It was founded in 1983 by Larry Wos, who served as its first Editor-in-Chief until 1992.

Scope

该刊致力于计算机逻辑推理的理论、实现与应用，关注领域横跨计算机科学、数学与哲学。稿件围绕以下方向展开：自动定理证明器与形式化证明助手等工具的开发和使用；模型检验器（model checker）等相关软件工具的设计；用于发现与表达形式证明的底层逻辑及其证明系统的理论性质；以及运用人工智能技术引导证明搜索的方法。科学界与工业界的应用都是极有价值的案例研究，可涉及硬件或软件的验证（用以确立正确性或安全性质）、数学的机械化等形式化工作。The journal is dedicated to the theory, implementation and applications of logical reasoning by computer. Its topics of interest connect computer science, mathematics and philosophy. They encompass the development and use of automatic theorem provers, formal proof assistants and related software tools such as model checkers, the design and study of the underlying logics and the theoretical properties of proof systems used to discover and express formal proofs, and the use of artificial intelligence techniques to guide the search for a proof. Scientific and industrial applications are invaluable as case studies, covering verification of hardware or software to establish correctness or security properties, the formalization of mathematics, and many other areas.^[1]

• 定理证明器与证明助手： 自动定理证明器、形式化证明助手（如 Lean、Coq、Isabelle 等系统）及其工程实现的进展。Theorem provers and proof assistants: advances in automatic theorem provers, formal proof assistants such as Lean, Coq and Isabelle, and their engineering implementations.
• 逻辑与证明系统理论： 形式系统、模型检验、可满足性判定与证明系统的可靠性与完备性等理论性质。Logic and proof theory: formal systems, model checking, satisfiability decision procedures, and theoretical properties such as soundness and completeness of proof systems.
• 数学机械化： 将数学证明形式化的工作，以及自动化推理在数学研究中的应用。Formalization of mathematics: the formalization of mathematical proofs and the application of automated reasoning in mathematical research.
• 软硬件验证： 以形式化方法验证关键系统的正确性、安全性与可靠性，包括认证与模型检验在工业界落地时的案例。Software and hardware verification: the use of formal methods to establish the correctness, safety and reliability of critical systems, including industrial case studies in certification and model checking.

期刊强调，成功的验证实践不仅能产出成果本身，也为如何更好地使用和增强这些工具提供经验积累，并指向一个未来：形式验证将成为关键计算基础设施以及数学、计算机科学等学科研究的常规手段。The journal emphasizes that successful verification efforts yield lessons on how to use the tools better and how to enhance them, and that they point to a future in which formal verification becomes routine for critical computing infrastructure and for research in mathematics, computer science and other disciplines that can benefit from the convenience and rigor of automated reasoning.

History

• 创刊与奠基期（1983—1992年）： 期刊于 1983 年由 Larry Wos 创办，他担任主编直至 1992 年；创刊之初聚焦于定理的机械验证，奠定了学科基础。Founding period (1983 to 1992): the journal was founded in 1983 by Larry Wos, who remained Editor-in-Chief until 1992. Its early focus on the mechanical verification of theorems established the field's intellectual base.
• 领域扩展与工具演进： 随着自动定理证明器与交互式证明助手的兴起，期刊的收稿范围从纯定理验证扩展到逻辑设计、模型检验与证明助手工程。Expansion of scope: with the rise of automated theorem provers and interactive proof assistants, the journal's scope broadened from pure theorem proving to logic design, model checking and proof-assistant engineering.
• 数字化与开放获取转型： 期刊转为混合获取模式，接收 ITP（Interactive Theorem Proving）等会议 Extended Papers，并在 SpringerLink 平台上以电子形式为主发行。Digitization and open-access transition: the journal moved to a hybrid model, began accepting Extended Papers from conferences such as the International Conference on Interactive Theorem Proving (ITP), and shifted to primarily electronic distribution on SpringerLink.

Editors

期刊设执行主编（Editor-in-Chief），由形式化方法与自动推理领域的学者担任，负责期刊整体方向与稿件的最终录用。The journal has an Editor-in-Chief drawn from the formal methods and automated reasoning community, responsible for the journal's overall direction and final acceptance of manuscripts.^[2]

• 执行主编： Jasmin Blanchette（慕尼黑大学，德国），理论计算机科学教授。Editor-in-Chief: Jasmin Blanchette, Professor of Theoretical Computer Science at the Ludwig-Maximilians-Universität München, Germany.
• 首任主编： Larry Wos（1983—1992 年在任），自动推理领域先驱，沃斯问题（Wos problem）与 Wos 算法的提出者。Founding Editor-in-Chief: Larry Wos (in post 1983 to 1992), a pioneer of automated reasoning known for the Wos problem and Wos algorithms.
• 编委阵容： 完整编委会名单与近期编委变动见期刊官网。Editorial board: the full list of board members and recent board changes are published on the journal's official website.