Cover Image

On proving consistency of equational theories in Bounded Arithmetic

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Beckmann, Arnold, Yamagata, Yoriyuki
Format:	Preprint
Published:	2022
Subjects:	Logic Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

On the Metric Temporal Logic for Continuous Stochastic Processes
by: Ikeda, Mitsumasa, et al.
Published: (2023)

Did Turing prove the undecidability of the halting problem?
by: Hamkins, Joel David, et al.
Published: (2024)

Unravelling Cyclic First-Order Arithmetic
by: Leigh, Graham E., et al.
Published: (2025)

The Arithmetical Hierarchy: A Realizability-Theoretic Perspective
by: Kihara, Takayuki
Published: (2024)

On the consistency of stronger lower bounds for NEXP
by: Thapen, Neil
Published: (2025)

A method for the automated generation of proof exercises with comparable levels of proving complexity
by: Mendes, João, et al.
Published: (2026)

Bringing closure to theory combination properties
by: Toledo, Guilherme V., et al.
Published: (2026)

Undecidability of theories of semirings with fixed points
by: Das, Anupam, et al.
Published: (2025)

Strong negation in the theory of computable functionals TCF
by: Köpp, Nils, et al.
Published: (2022)

Access Hoare Logic
by: Beckmann, Arnold, et al.
Published: (2025)

Being polite is not enough (and other limits of theory combination)
by: Toledo, Guilherme V., et al.
Published: (2025)

The proof theory and semantics of second-order (intuitionistic) tense logic
by: Becker, Justus, et al.
Published: (2026)

An abstract fixed-point theorem for Horn formula equations
by: Hetzl, Stefan, et al.
Published: (2025)

Wider systems for linear logic with fixed points: proof theory and complexity
by: Das, Anupam, et al.
Published: (2026)

Domain theory in univalent foundations I: Directed complete posets and Scott's $D_\infty$
by: de Jong, Tom
Published: (2024)

A proof theory of (omega-)context-free languages, via non-wellfounded proofs
by: Das, Anupam, et al.
Published: (2024)

MCSAT Modulo Transcendental Arithmetics
by: Gallego-Hernández, Jorge, et al.
Published: (2026)

Peano Arithmetic and $μ$MALL
by: Manighetti, Matteo, et al.
Published: (2023)

Towards an Analysis of Proofs in Arithmetic
by: Leitsch, Alexander, et al.
Published: (2025)

On the Decidability of Monadic Theories of Arithmetic Predicates
by: Berthé, Valérie, et al.
Published: (2024)

Nonlinear Arithmetic with SMTLIB Division is Undecidable
by: Jovanovic, Dejan
Published: (2026)

Satisfiability Modulo Exponential Integer Arithmetic
by: Frohn, Florian, et al.
Published: (2024)

On the Decidability of Presburger Arithmetic Expanded with Powers
by: Karimov, Toghrul, et al.
Published: (2024)

The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory
by: de Jong, Tom, et al.
Published: (2026)

Incorrectness Separation Logic with Arrays and Pointer Arithmetic
by: Lee, Yeonseok, et al.
Published: (2025)

Resource-Bounded Type Theory: Compositional Cost Analysis via Graded Modalities
by: Mannucci, Mirco A., et al.
Published: (2025)

Resource-Bounded Martin-Löf Type Theory: Compositional Cost Analysis for Dependent Types
by: Mannucci, Mirco A., et al.
Published: (2026)

Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions
by: Su, Wanyun, et al.
Published: (2024)

Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic
by: Ito, Sohei, et al.
Published: (2025)

Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
by: Hozzová, Petra, et al.
Published: (2024)

Homotopy type theory as a language for diagrams of $\infty$-logoses
by: Uemura, Taichi
Published: (2022)

Formalizing two-level type theory with cofibrant exo-nat
by: Uskuplu, Elif
Published: (2023)

Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search
by: Lipparini, Enrico, et al.
Published: (2025)

Satisfiability of Non-Linear Transcendental Arithmetic as a Certificate Search Problem
by: Lipparini, Enrico, et al.
Published: (2023)

Yet another cubical type theory, but via a semantic approach
by: Kapulkin, Chris, et al.
Published: (2025)

Relating homotopy equivalences to conservativity in dependent type theories with computation axioms
by: Spadetto, Matteo
Published: (2023)

Feasibility of Primality in Bounded Arithmetic
by: Jalali, Raheleh, et al.
Published: (2025)

Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic (Technical Report)
by: Habermehl, Peter, et al.
Published: (2024)

Forbidden Induced Subgraphs for Bounded Shrub-Depth and the Expressive Power of MSO
by: Mählmann, Nikolas
Published: (2025)

Towards Automated Verification of Logarithmic Arithmetic
by: Arnold, Mark G., et al.
Published: (2024)