Skip to main content

Journal of Automated Reasoning

Ausgabe 4/2023

Inhalt (8 Artikel)

Enabling Floating-Point Arithmetic in the Coq Proof Assistant

Érik Martin-Dorel, Guillaume Melquiond, Pierre Roux

Research

Combining Stable Infiniteness and (Strong) Politeness

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark Barrett, Cesare Tinelli

Open Access

Lower Bounds for QCDCL via Formula Gauge

Benjamin Böhm, Olaf Beyersdorff

Open Access

Finitary Type Theories With and Without Contexts

Philipp G. Haselwarter, Andrej Bauer

Self-evident Automated Geometric Theorem Proving Based on Complex Number Identity

Xicheng Peng, Jingzhong Zhang, Mao Chen, Sannyuya Liu

Formal Verification of Termination Criteria for First-Order Recursive Functions

Cesar A. Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron M. Dutle, Anthony J. Narkawicz, Ariane Alves Almeida, Andréia B. Avelar da Silva, Thiago M. Ferreira Ramos