-
A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic
Authors:
Simon Docherty,
Reuben N. S. Rowe
Abstract:
We define a infinitary labelled sequent calculus for PDL, G3PDL^{\infty}. A finitarily representable cyclic system, G3PDL^ω, is then given. We show that both are sound and complete with respect to standard models of PDL and, further, that G3PDL^{\infty} is cut-free complete. We additionally investigate proof-search strategies in the cyclic system for the fragment of PDL without tests.
We define a infinitary labelled sequent calculus for PDL, G3PDL^{\infty}. A finitarily representable cyclic system, G3PDL^ω, is then given. We show that both are sound and complete with respect to standard models of PDL and, further, that G3PDL^{\infty} is cut-free complete. We additionally investigate proof-search strategies in the cyclic system for the fragment of PDL without tests.
△ Less
Submitted 16 May, 2019; v1 submitted 15 May, 2019;
originally announced May 2019.
-
Infinitary and Cyclic Proof Systems for Transitive Closure Logic
Authors:
Liron Cohen,
Reuben N. S. Rowe
Abstract:
Transitive closure logic is a known extension of first-order logic obtained by introducing a transitive closure operator. While other extensions of first-order logic with inductive definitions are a priori parametrized by a set of inductive definitions, the addition of the transitive closure operator uniformly captures all finitary inductive definitions. In this paper we present an infinitary proo…
▽ More
Transitive closure logic is a known extension of first-order logic obtained by introducing a transitive closure operator. While other extensions of first-order logic with inductive definitions are a priori parametrized by a set of inductive definitions, the addition of the transitive closure operator uniformly captures all finitary inductive definitions. In this paper we present an infinitary proof system for transitive closure logic which is an infinite descent-style counterpart to the existing (explicit induction) proof system for the logic. We show that, as for similar systems for first-order logic with inductive definitions, our infinitary system is complete for the standard semantics and subsumes the explicit system. Moreover, the uniformity of the transitive closure operator allows semantically meaningful complete restrictions to be defined using simple syntactic criteria. Consequently, the restriction to regular infinitary (i.e. cyclic) proofs provides the basis for an effective system for automating inductive reasoning.
△ Less
Submitted 28 June, 2018; v1 submitted 2 February, 2018;
originally announced February 2018.
-
Size Relationships in Abstract Cyclic Entailment Systems
Authors:
Reuben N. S. Rowe,
James Brotherston
Abstract:
A cyclic proof system generalises the standard notion of a proof as a finite tree of locally sound inferences by allowing proof objects to be potentially infinite. Regular infinite proofs can be finitely represented as graphs. To preclude spurious cyclic reasoning, cyclic proof systems come equipped with a well-founded notion of 'size' for the models that interpret their logical statements. A glob…
▽ More
A cyclic proof system generalises the standard notion of a proof as a finite tree of locally sound inferences by allowing proof objects to be potentially infinite. Regular infinite proofs can be finitely represented as graphs. To preclude spurious cyclic reasoning, cyclic proof systems come equipped with a well-founded notion of 'size' for the models that interpret their logical statements. A global soundness condition on proof objects, stated in terms of this notion of size, ensures that any non-well-founded paths in the proof object can be disregarded.
We give an abstract definition of a subclass of such cyclic proof systems: cyclic entailment systems. In this setting, we consider the problem of comparing the size of a model when interpreted in relation to the antecedent of an entailment, with that when interpreted in relation to the consequent. Specifically, we give a further condition on proof objects which ensures that models of a given entailment are always 'smaller' when interpreted with respect to the consequent than when interpreted with respect to the antecedent. Knowledge of such relationships is useful in a program verification setting.
△ Less
Submitted 13 February, 2017;
originally announced February 2017.
-
Encoding the Factorisation Calculus
Authors:
Reuben N. S. Rowe
Abstract:
Jay and Given-Wilson have recently introduced the Factorisation (or SF-) calculus as a minimal fundamental model of intensional computation. It is a combinatory calculus containing a special combinator, F, which is able to examine the internal structure of its first argument. The calculus is significant in that as well as being combinatorially complete it also exhibits the property of structural c…
▽ More
Jay and Given-Wilson have recently introduced the Factorisation (or SF-) calculus as a minimal fundamental model of intensional computation. It is a combinatory calculus containing a special combinator, F, which is able to examine the internal structure of its first argument. The calculus is significant in that as well as being combinatorially complete it also exhibits the property of structural completeness, i.e. it is able to represent any function on terms definable using pattern matching on arbitrary normal forms. In particular, it admits a term that can decide the structural equality of any two arbitrary normal forms.
Since SF-calculus is combinatorially complete, it is clearly at least as powerful as the more familiar and paradigmatic Turing-powerful computational models of Lambda Calculus and Combinatory Logic. Its relationship to these models in the converse direction is less obvious, however. Jay and Given-Wilson have suggested that SF-calculus is strictly more powerful than the aforementioned models, but a detailed study of the connections between these models is yet to be undertaken.
This paper begins to bridge that gap by presenting a faithful encoding of the Factorisation Calculus into the Lambda Calculus preserving both reduction and strong normalisation. The existence of such an encoding is a new result. It also suggests that there is, in some sense, an equivalence between the former model and the latter. We discuss to what extent our result constitutes an equivalence by considering it in the context of some previously defined frameworks for comparing computational power and expressiveness.
△ Less
Submitted 26 August, 2015;
originally announced August 2015.
-
Semantic Predicate Types and Approximation for Class-based Object Oriented Programming
Authors:
Steffen van Bakel,
Reuben N. S. Rowe
Abstract:
We apply the principles of the intersection type discipline to the study of class-based object oriented programs and; our work follows from a similar approach (in the context of Abadi and Cardelli's Varsigma-object calculus) taken by van Bakel and de'Liguoro. We define an extension of Featherweight Java, FJc and present a predicate system which we show to be sound and expressive. We also show that…
▽ More
We apply the principles of the intersection type discipline to the study of class-based object oriented programs and; our work follows from a similar approach (in the context of Abadi and Cardelli's Varsigma-object calculus) taken by van Bakel and de'Liguoro. We define an extension of Featherweight Java, FJc and present a predicate system which we show to be sound and expressive. We also show that our system provides a semantic underpinning for the object oriented paradigm by generalising the concept of approximant from the Lambda Calculus and demonstrating an approximation result: all expressions to which we can assign a predicate have an approximant that satisfies the same predicate. Crucial to this result is the notion of predicate language, which associates a family of predicates with a class.
△ Less
Submitted 21 September, 2011;
originally announced September 2011.
