University of Illinois Urbana-Champaign

Technical Report: A Logical Treatment

Rodrigues, Nishant; Sebe, Mircea Octavian; Chen, Xiaohong; Rosu, Grigore

Content Files
a-logical-treatment-of-finite-automata.pdf

Permalink

https://hdl.handle.net/2142/121770

Description

Title
Technical Report: A Logical Treatment
Author(s)
  • Rodrigues, Nishant
  • Sebe, Mircea Octavian
  • Chen, Xiaohong
  • Rosu, Grigore
Issue Date
2024-04-01
Keyword(s)
  • matching logic
  • automata
  • induction
Date of Ingest
2024-01-27T05:43:27-06:00
Abstract
We present a sound and complete axiomatization of finite words using matching logic. A unique feature of our axiomatization is that it gives a *shallow embedding* of regular expressions into matching logic, and a *logical* representation of finite automata. The semantics of both expressions and automata are precisely captured as matching logic formulae that evaluate to the corresponding language. Regular expressions are matching logic formulae *as is*, while the embedding of automata is a *structural analog*---computational aspects of automata are captured as syntactic features. We demonstrate that our axiomatization is sound and complete by showing that runs of Brzozowski's procedure for equivalence checking correspond to matching logic proofs. We propose this as a general methodology for producing machine-checkable formal proofs, enabled by capturing structural analogs of computational artifacts in logic. The proofs produced can be efficiently checked by the Metamath Zero verifier. Work presented in this paper contributes to the general scheme of achieving verifiable computing via logical methods, where computations are reduced to logical reasoning, encoded as machine-checkable proof objects, and checked by a trusted proof checker.
Type of Resource
text
Language
eng

Owning Collections

Research and Tech Reports - Computer Science PRIMARY