Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 0708.2252

Focusing and Polarization in Intuitionistic Logic

Chuck Liang·Dale Miller
View original source ↗Read source document ↗Export metadata ↓

Abstract

A focused proof system provides a normal form to cut-free proofs that structures the application of invertible and non-invertible inference rules. The focused proof system of Andreoli for linear logic has been applied to both the proof search and the proof normalization approaches to computation. Various proof systems in literature exhibit characteristics of focusing to one degree or another. We present a new, focused proof system for intuitionistic logic, called LJF, and show how other proof systems can be mapped into the new system by inserting logical connectives that prematurely stop focusing. We also use LJF to design a focused proof system for classical logic. Our approach to the design and analysis of these systems is based on the completeness of focusing in linear logic and on the notion of polarity that appears in Girard's LC and LU proof systems.

Explore related subjects

cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Chuck Liang, Dale Miller. 2007-08-16. Focusing and Polarization in Intuitionistic Logic. https://arxiv.org/abs/0708.2252

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Decisiveness for countable MDPs and insights for NPLCSs and POMDPs

Markov chains and Markov decision processes (MDPs) are well-established probabilistic models. While finite Markov models are well-understood, analysing their infinite counterparts remains a significant challenge. Decisiveness has proved to be an elegant property for countable Markov chains: it is general enough to be satisfied by several natural classes of countable Markov chains, and it guarantees the termination of simple qualitative and approximate quantitative model-checking algorithms. In contrast, existing work on the formal analysis of countable MDPs usually relies on ad hoc techniques tailored to specific classes. In this paper, we provide a general framework to analyse countable MDPs (with finitely many enabled actions per state) by extending the notion of decisiveness. Compared to Markov chains, MDPs exhibit an additional nondeterministic choice that can be resolved in an adversarial or cooperative way, leading to multiple natural notions of decisiveness. We show that these notions enable the approximation of supremum reachability and infimum reachability (equivalently, supremum safety) probabilities in countable MDPs using generic approximation schemes. We then instantiate our generic approach to two concrete classes of models inducing countable MDPs: nondeterministic probabilistic lossy channel systems (NPLCSs) and partially observable MDPs (POMDPs). This leads to concrete algorithms to compute approximations to supremum safety probabilities in each of these classes.

cs.LO↗
arXiv2026

Complete Dynamic Logic of Communicating Hybrid Programs

This article presents a relatively complete proof calculus for the dynamic logic of communicating hybrid programs dLCHP. Beyond hybrid systems, communicating hybrid programs not only feature mixed discrete and continuous dynamics but also their parallel interactions in parallel hybrid systems. This not only combines the subtleties of hybrid and discrete parallel systems, but parallel hybrid dynamics necessitates that all parallel subsystems synchronize in time and evolve truly simultaneously. To enable compositional reasoning nevertheless, dLCHP combines differential dynamic logic dL with mutual abstraction of subsystems by assumption-commitment (ac) reasoning. The resulting proof calculus preserves the essence of dynamic logic axiomatizations, while revealing-and being driven by-a new modal logic view onto ac-reasoning. The dLCHP proof calculus is shown to be complete relative to $Ω$-FOD, the first-order logic of differential equation properties FOD augmented with communication traces. This confirms that the calculus covers all aspects of parallel hybrid systems, because it lacks no axioms to reduce all their dynamical effects to the assertion logic. Additional axioms for encoding communication traces enable a provably correct equitranslation between $Ω$-FOD and FOD, which reveals the possibility of representational succinctness in parallel hybrid systems proofs. Transitively, this establishes a full proof-theoretical alignment of dLCHP and dL, and shows that reasoning about parallel hybrid systems is exactly as hard as reasoning about hybrid systems, continuous systems, or discrete systems.

cs.LO↗
arXiv2026

Overview and Roadmap of Team Automata

Team Automata is a formalism for interacting component-based systems proposed in 1997, whereby multiple sending and receiving actions from concurrent automata can synchronise. During the past 25+ years, team automata have been studied and applied in many different contexts, involving 25+ researchers and resulting in 25+ publications. In this paper, we first revisit the specific notion of synchronisation and composition of team automata, relating it to other relevant coordination models, such as Reo, BIP, Contract Automata, Choreography Automata, and Multi-Party Session Types. We then identify several aspects that have recently been investigated for team automata and related models. These include communication properties (which are the properties of interest?), realisability (how to decompose a global model into local components?), tool support (what has been automatised or implemented?), and variability (can a family of concrete product (automata) models be captured concisely?). Our presentation of these aspects provides a snapshot of the most recent trends in research on team automata, and delineates a roadmap for future research, both for team automata and for related formalisms.

cs.LO↗