David Pym
YOU?
Author Swipe
View article: Bifurcation Logic: Separation Through Ordering
Bifurcation Logic: Separation Through Ordering Open
We introduce Bifurcation Logic, BL, which combines a basic classical modality with separating conjunction * together with its naturally associated multiplicative implication, that is defined using the modal ordering. Specifically, a formul…
View article: Base-Extension Semantics for Intuitionistic Modal Logics (Extended Abstract)
Base-Extension Semantics for Intuitionistic Modal Logics (Extended Abstract) Open
The proof theory and semantics of intuitionistic modal logics have been studied by Simpson in terms of Prawitz-style labelled natural deduction systems and Kripke models. An alternative to model-theoretic semantics is provided by proof-the…
View article: Proof-theoretic Semantics for Second-order Logic
Proof-theoretic Semantics for Second-order Logic Open
We develop a proof-theoretic semantics (P-tS) for second-order logic (S-oL), providing an inferentialist alternative to both full and Henkin model-theoretic interpretations. Our approach is grounded in base-extension semantics (B-eS), a fr…
View article: Proof-theoretic Semantics for the Logic of Bunched Implications
Proof-theoretic Semantics for the Logic of Bunched Implications Open
The logic of bunched implications (BI) can be seen as the free combination of intuitionistic propositional logic (IPL) and intuitionistic multiplicative linear logic (IMLL). We present here a base-extension semantics (B-eS) for BI in the s…
View article: Base-extension Semantics for Intuitionistic Modal Logics
Base-extension Semantics for Intuitionistic Modal Logics Open
The proof theory and semantics of intuitionistic modal logics have been studied by Simpson in terms of Prawitz-style labelled natural deduction systems and Kripke models. An alternative to model-theoretic semantics is provided by proof-the…
View article: Semantic Foundations of Reductive Reasoning
Semantic Foundations of Reductive Reasoning Open
The development of logic has largely been through the deductive paradigm: conclusions are inferred from established premisses. However, the use of logic in the context of both human and machine reasoning is typically through the dual reduc…
View article: Base-extension semantics for S5 modal logic
Base-extension semantics for S5 modal logic Open
We develop a proof-theoretic semantics—in particular, a base-extension semantics—for multi-agent $S5$ modal logic (and hence also for the usual unindexed $S5$). Following the inferentialist interpretation of logic, this gives us a semantic…
View article: From Proof-Theoretic Validity to Base-Extension Semantics for Intuitionistic Propositional Logic
From Proof-Theoretic Validity to Base-Extension Semantics for Intuitionistic Propositional Logic Open
Proof-theoretic semantics (P-tS) is the approach to meaning in logic based on proof (as opposed to truth). There are two major approaches to P-tS: proof-theoretic validity (P-tV) and base-extension semantics (B-eS). The former is a semanti…
View article: Modelling and simulating organizational ransomware recovery: structure, methodology, and decisions
Modelling and simulating organizational ransomware recovery: structure, methodology, and decisions Open
The problem of maintaining organizational resilience in the face of ransomware attacks represents an important issue for modern organizations. Organizational networks and IT infrastructure have become increasingly complex, and it is often …
View article: Co-designing heterogeneous models: a distributed systems approach
Co-designing heterogeneous models: a distributed systems approach Open
The nature of information security has been, and probably will continue to be, marked by the asymmetric competition of attackers and defenders over the control of an uncertain environment. The reduction of this degree of uncertainty via an…
View article: Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic
Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic Open
Proof-theoretic semantics (P-tS) is an innovative approach to grounding logical meaning in terms of proofs rather than traditional truth-conditional semantics. The point is not that one provides a proof system, but rather that one articula…
View article: Semantic Foundations of Reductive Reasoning
Semantic Foundations of Reductive Reasoning Open
The development of logic has largely been through the 'deductive' paradigm: conclusions are inferred from established premisses. However, the use of logic in the context of both human and machine reasoning is typically through the dual 're…
View article: Inferentialist Resource Semantics
Inferentialist Resource Semantics Open
In systems modelling, a 'system' typically comprises located resources relative to which processes execute. One important use of logic in informatics is in modelling such systems for the purpose of reasoning (perhaps automated) about their…
View article: Inferentialist Public Announcement Logic: Base-extension Semantics
Inferentialist Public Announcement Logic: Base-extension Semantics Open
Proof-theoretic semantics, and base-extension semantics in particular, can be seen as a logical realization of inferentialism, in which the meaning of expressions is understood through their use. We present a base-extension semantics for p…
View article: Co-designing heterogeneous models: a distributed systems approach
Co-designing heterogeneous models: a distributed systems approach Open
The nature of information security has been, and probably will continue to be, marked by the asymmetric competition of attackers and defenders over the control of an uncertain environment. The reduction of this degree of uncertainty via an…
View article: A Note on an Inferentialist Approach to Resource Semantics
A Note on an Inferentialist Approach to Resource Semantics Open
A central concept within informatics is in modelling such systems for the purpose of reasoning (perhaps automated) about their behaviour and properties. To this end, one requires an interpretation of logical formulae in terms of the resour…
View article: Base-extension Semantics for S5 Modal Logic
Base-extension Semantics for S5 Modal Logic Open
We develop a proof-theoretic semantics -- in particular, a base-extension semantics -- for multi-agent S5 modal logic (and hence also for the usual unindexed S5). Following the inferentialist interpretation of logic, this gives us a semant…
View article: A Note on the Practice of Logical Inferentialism
A Note on the Practice of Logical Inferentialism Open
A short essay presenting the State-Effect Interpretation of natural deduction rules as an explanatory framework for recent developments in proof-theoretic semantics.
View article: Base-extension semantics for modal logic
Base-extension semantics for modal logic Open
In proof-theoretic semantics, meaning is based on inference. It may seen as the mathematical expression of the inferentialist interpretation of logic. Much recent work has focused on base-extension semantics, in which the validity of formu…
View article: Inferentialist Resource Semantics
Inferentialist Resource Semantics Open
In systems modelling, a 'system' typically comprises located resources relative to which processes execute. One important use of logic in informatics is in modelling such systems for the purpose of reasoning (perhaps automated) about their…
View article: Base-extension Semantics for Modal Logic
Base-extension Semantics for Modal Logic Open
In proof-theoretic semantics, meaning is based on inference. It may seen as the mathematical expression of the inferentialist interpretation of logic. Much recent work has focused on base-extension semantics, in which the validity of formu…
View article: ‘The trivial tickets build the trust’: a co-design approach to understanding security support interactions in a large university
‘The trivial tickets build the trust’: a co-design approach to understanding security support interactions in a large university Open
Increasingly, organizations are acknowledging the importance of human factors in the management of security in workplaces. There are challenges in managing security infrastructures in which there may be centrally mandated and locally manag…
View article: Proof-theoretic Semantics for the Logic of Bunched Implications
Proof-theoretic Semantics for the Logic of Bunched Implications Open
The logic of bunched implications (BI) can be seen as the free combination of intuitionistic propositional logic (IPL) and intuitionistic multiplicative linear logic (IMLL). We present here a base-extension semantics (B-eS) for BI in the s…
View article: Defining logical systems via algebraic constraints on proofs
Defining logical systems via algebraic constraints on proofs Open
We present a comprehensive programme analysing the decomposition of proof systems for non-classical logics into proof systems for other logics, especially classical logic, using an algebra of constraints. That is, one recovers a proof syst…
View article: Definite Formulae, Negation-as-Failure, and the Base-Extension Semantics of Intuitionistic Propositional Logic
Definite Formulae, Negation-as-Failure, and the Base-Extension Semantics of Intuitionistic Propositional Logic Open
Proof-theoretic semantics (P-tS) is the paradigm of semantics in which meaning in logic is based on proof (as opposed to truth). A particular instance of P-tS for intuitionistic propositional logic (IPL) is its base-extension semantics (B-…
View article: Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract)
Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract) Open
This work is the first exploration of proof-theoretic semantics for a substructural logic. It focuses on the base-extension semantics (B-eS) for intuitionistic multiplicative linear logic (IMLL). The starting point is a review of Sandqvist…
View article: Categorical Proof-Theoretic Semantics
Categorical Proof-Theoretic Semantics Open
In proof-theoretic semantics, model-theoretic validity is replaced by proof-theoretic validity. Validity of formulae is defined inductively from a base giving the validity of atoms using inductive clauses derived from proof-theoretic rules…