Showing 1–6 of 6 results for author: Simmons, R J

Finite-Choice Logic Programming

Authors: Robert J. Simmons, Michael Arntzenius, Chris Martens

Abstract: Logic programming, as exemplified by datalog, defines the meaning of a program as the canonical smallest model derived from deductive closure over its inference rules. However, many problems call for an enumeration of models that vary along some set of choices while maintaining structural and logical constraints -- there is no single canonical model. The notion of stable models has successfully ca… ▽ More Logic programming, as exemplified by datalog, defines the meaning of a program as the canonical smallest model derived from deductive closure over its inference rules. However, many problems call for an enumeration of models that vary along some set of choices while maintaining structural and logical constraints -- there is no single canonical model. The notion of stable models has successfully captured programmer intuition about the set of valid solutions for such problems, giving rise to a family of programming languages and associated solvers collectively known as answer set programming. Unfortunately, the definition of a stable model is frustratingly indirect, especially in the presence of rules containing free variables. We propose a new formalism, called finite-choice logic programing, for which the set of stable models can be characterized as the least fixed point of an immediate consequence operator. Our formalism allows straightforward expression of common idioms in both datalog and answer set programming, gives meaning to a new and useful class of programs, enjoys a constructive and direct operational semantics, and admits a predictive cost semantics, which we demonstrate through our implementation. △ Less

Submitted 29 May, 2024; originally announced May 2024.

Relating Reasoning Methodologies in Linear Logic and Process Algebra

Authors: Yuxin Deng, Iliano Cervesato, Robert J. Simmons

Abstract: We show that the proof-theoretic notion of logical preorder coincides with the process-theoretic notion of contextual preorder for a CCS-like calculus obtained from the formula-as-process interpretation of a fragment of linear logic. The argument makes use of other standard notions in process algebra, namely a labeled transition system and a coinductively defined simulation relation. This result… ▽ More We show that the proof-theoretic notion of logical preorder coincides with the process-theoretic notion of contextual preorder for a CCS-like calculus obtained from the formula-as-process interpretation of a fragment of linear logic. The argument makes use of other standard notions in process algebra, namely a labeled transition system and a coinductively defined simulation relation. This result establishes a connection between an approach to reason about process specifications and a method to reason about logic specifications. △ Less

Submitted 17 November, 2012; originally announced November 2012.

Comments: In Proceedings LINEARITY 2012, arXiv:1211.3480

Journal ref: Math. Struct. Comp. Sci. 26 (2016) 868-906

Constructive Provability Logic

Authors: Robert J. Simmons, Bernardo Toninho

Abstract: We present constructive provability logic, an intuitionstic modal logic that validates the Löb rule of Gödel and Löb's provability logic by permitting logical reflection over provability. Two distinct variants of this logic, CPL and CPL*, are presented in natural deduction and sequent calculus forms which are then shown to be equivalent. In addition, we discuss the use of constructive provability… ▽ More We present constructive provability logic, an intuitionstic modal logic that validates the Löb rule of Gödel and Löb's provability logic by permitting logical reflection over provability. Two distinct variants of this logic, CPL and CPL*, are presented in natural deduction and sequent calculus forms which are then shown to be equivalent. In addition, we discuss the use of constructive provability logic to justify stratified negation in logic programming within an intuitionstic and structural proof theory. △ Less

Submitted 29 May, 2012; originally announced May 2012.

Comments: Extended version of IMLA 2011 submission of the same title

MSC Class: 03F05; 03B45; 03F45 ACM Class: F.4.1; I.2.3

Structural focalization

Authors: Robert J. Simmons

Abstract: Focusing, introduced by Jean-Marc Andreoli in the context of classical linear logic, defines a normal form for sequent calculus derivations that cuts down on the number of possible derivations by eagerly applying invertible rules and grou** sequences of non-invertible rules. A focused sequent calculus is defined relative to some non-focused sequent calculus; focalization is the property that eve… ▽ More Focusing, introduced by Jean-Marc Andreoli in the context of classical linear logic, defines a normal form for sequent calculus derivations that cuts down on the number of possible derivations by eagerly applying invertible rules and grou** sequences of non-invertible rules. A focused sequent calculus is defined relative to some non-focused sequent calculus; focalization is the property that every non-focused derivation can be transformed into a focused derivation. In this paper, we present a focused sequent calculus for propositional intuitionistic logic and prove the focalization property relative to a standard presentation of propositional intuitionistic logic. Compared to existing approaches, the proof is quite concise, depending only on the internal soundness and completeness of the focused logic. In turn, both of these properties can be established (and mechanically verified) by structural induction in the style of Pfenning's structural cut elimination without the need for any tedious and repetitious invertibility lemmas. The proof of cut admissibility for the focused system, which establishes internal soundness, is not particularly novel. The proof of identity expansion, which establishes internal completeness, is a major contribution of this work. △ Less

Submitted 16 March, 2014; v1 submitted 28 September, 2011; originally announced September 2011.

Comments: A Twelf formalization is included and an Agda formalization is available at https://github.com/robsimmons/agda-lib/tree/focalization

MSC Class: 03F05; 03F07; 03F65 ACM Class: F.4.1

Products of Weighted Logic Programs

Authors: Shay B. Cohen, Robert J. Simmons, Noah A. Smith

Abstract: Weighted logic programming, a generalization of bottom-up logic programming, is a well-suited framework for specifying dynamic programming algorithms. In this setting, proofs correspond to the algorithm's output space, such as a path through a graph or a grammatical derivation, and are given a real-valued score (often interpreted as a probability) that depends on the real weights of the base axiom… ▽ More Weighted logic programming, a generalization of bottom-up logic programming, is a well-suited framework for specifying dynamic programming algorithms. In this setting, proofs correspond to the algorithm's output space, such as a path through a graph or a grammatical derivation, and are given a real-valued score (often interpreted as a probability) that depends on the real weights of the base axioms used in the proof. The desired output is a function over all possible proofs, such as a sum of scores or an optimal score. We describe the PRODUCT transformation, which can merge two weighted logic programs into a new one. The resulting program optimizes a product of proof scores from the original programs, constituting a scoring function known in machine learning as a ``product of experts.'' Through the addition of intuitive constraining side conditions, we show that several important dynamic programming algorithms can be derived by applying PRODUCT to weighted logic programs corresponding to simpler weighted logic programs. In addition, we show how the computation of Kullback-Leibler divergence, an information-theoretic measure, can be interpreted using PRODUCT. △ Less

Submitted 15 June, 2010; originally announced June 2010.

Journal ref: TLP 11 (2-3): 263-296, 2011

Magnetic Field Induced Charged Exciton Studies in a GaAs/Al(0.3)Ga(0.7)As Single Heterojunction

Authors: F. M. Munteanu, Yongmin Kim, C. H. Perry, D. G. Rickel J. A. Simmons, J. L. Reno

Abstract: The magnetophotoluminescence (MPL) behavior of a GaAs/Al(0.3)Ga(0.7)As single heterojunction has been investigated to 60T. We observed negatively charged singlet and triplet exciton states that are formed at high magnetic fields beyond the nu=1 quantum Hall state. The variation of the charged exciton binding energies are in good agreement with theoretical predictions. The MPL transition intensit… ▽ More The magnetophotoluminescence (MPL) behavior of a GaAs/Al(0.3)Ga(0.7)As single heterojunction has been investigated to 60T. We observed negatively charged singlet and triplet exciton states that are formed at high magnetic fields beyond the nu=1 quantum Hall state. The variation of the charged exciton binding energies are in good agreement with theoretical predictions. The MPL transition intensities for these states showed intensity variations (maxima and minima) at the nu=1/3 and 1/5 fractional quantum Hall (FQH) state as a consequence of a large reduction of electron-hole screening at these filling factors. △ Less

Submitted 19 May, 1999; originally announced May 1999.

Comments: submitted to Phys. Rev. Lett