Abstract We formalise tableau procedures for the modal logics K, KT, and S4, and the modal fixpoint logic LTL, in the proof assistant Coq version 8.17.1. This involves encoding the algorithms, and formally proving their termination and their correctness, the latter boiling down to showing that they are both sound and complete with respect to the semantics of these logics. We give a quick overview of our account of S4 because most of the work had already been achieved by Wu and Goré then focus on LTL: we describe the rules of our tableau calculus and our approach to formally verify it in Coq. Unlike K and KT, these logics require checking for loops and need particular attention to build a satisfying model. Moreover, for LTL, we must also distinguish “good loops” from “bad loops” due to the presence of least and greatest fixpoint modalities. We show how we manage to implement loop-checks to ensure termination and how a model can be constructed from their tableau tree in order to prove soundness. We also demonstrate how the eventuality formulae of LTL are handled in the tableau rules and the various proofs. Such algorithms encoded in Coq can easily be modified to output a satisfying model in the case where the input is satisfiable. We use the program extraction feature of Coq to produce source code for the verified tableau procedures in OCaml and compile them to obtain actual executable programs. We then evaluate these verified programs on the standard benchmarks against other reasoners which are optimised but unverified. As expected, the results show a clear inferiority of our verified reasoners in terms of efficiency, however they still demonstrate that we can be optimistic regarding the usability of verified reasoners in practice. Wu, M., Goré, R.: Verified decision procedures for modal logics.

Abstract We extend the mono-modal CEGAR-tableaux of Goré and Kikkert to normal multi-modal logic $$\textrm{K}_{\textrm{n}}$$ K n with global assumptions. We then extend these CEGAR-tableaux to multi-modal tense logic $$\textrm{Kt}_{\textrm{n}}$$ Kt n without global assumptions by “compiling in” the residuation conditions between “future” and “past” modalities. Our new implementation uses $$\mathrm {C^{++}}$$ C + + and includes multiple optimisations which speed up proof-search. $$\texttt {CEGARBox++}$$ CEGARBox + + is the best satisfiability-checker for mono-modal tense logic $$\textrm{Kt}_{\textrm{1}}$$ Kt 1 but is not competitive for global assumptions.

Abstract We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong Löb logic $$\textsf{iSL}$$ , an intuitionistic modal logic with a provability interpretation. A novel measure on sequents is used to prove both the termination of the naive backward proof search strategy, and the admissibility of cut in a syntactic and direct way, leading to a straightforward cut-elimination procedure. All proofs have been formalised in the interactive theorem prover Coq.

Verifiable mix nets, and specifically proofs of (correct) shuffle, are a fundamental building block in numerous applications: these zero-knowledge proofs allow the prover to produce a public transcript which can be perused by the verifier to confirm the purported shuffle. They are particularly vital to verifiable electronic voting, where they underpin almost all voting schemes with non-trivial tallying methods. These complicated pieces of cryptography are a prime location for critical errors which might allow undetected modification of the outcome.The best solution to preventing these errors is to machine-check the cryptographic properties of the design and implementation of the mix net. Particularly crucial for the integrity of the outcome is the soundness of the design and implementation of the verifier (software). Unfortunately, several different encryption schemes are used in many different slight variations which makes it infeasible to machine-check every single case individually. However, a particular optimised variant of the Terelius-Wikström mix net is, and has been, widely deployed in elections including national elections in Norway, Estonia and Switzerland, albeit with many slight variations and several different encryption schemes.In this work, we develop the logical theory and formal methods tools to machine-check the design and implementation of all these variants of Terelius-Wikström mix nets, for all the different encryption schemes used; resulting in provably correct mix nets for all these different variations. We do this carefully to ensure that we can extract a formally verified implementation of the verifier (software) which is compatible with existing deployed implementations of the Terelius-Wikström mix net. This gives us provably correct implementations of the verifiers for more than half of the national elections which have used verifiable mix nets.Our implementation of a proof of correct shuffle is the first to be machine-checked to be cryptographically correct and able to verify proof transcripts from national elections. We demonstrate the practicality of our implementation by verifying transcripts produced by the Verificatum mix net system and the CHVote e-voting system from Switzerland.

We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequent calculus, but have all been shown to have cut-free nested sequent calculi. The proof of the interpolation theorem uses these calculi and is purely syntactic, without resorting to embeddings, semantic arguments, or interpreted connectives external to the underlying logical language. A novel feature of our proof includes an orthogonality condition for defining duality between interpolants.

The security and trustworthiness of elections is critical to democracy; alas, securing elections is notoriously hard. Powerful cryptographic techniques for verifying the integrity of electronic voting have been developed and are in increasingly common use. The claimed security guarantees of most of these techniques have been formally proved. However, implementing the cryptographic verifiers which utilize these techniques is a technical and error prone process, and often leads to critical errors appearing in the gap between the implementation and the formally verified design. We significantly reduce the gap between theory and practice by using machine checked proofs coupled with code extraction to produce cryptographic verifiers that are themselves formally verified. We demonstrate the feasibility of our technique by producing a formally verified verifier which we use to check the 2018 International Association for Cryptologic Research (IACR) directors election.

The mathematical framework of Stone duality is used to synthesize a number of hitherto separate developments in Theoretical Computer Science: - Domain Theory, the mathematical theory of computation introduced by Scott as a foundation for denotational semantics. - The theory of concurrency and systems behaviour developed by Milner, Hennessy et al. based on operational semantics. - Logics of programs. Stone duality provides a junction between semantics (spaces of points = denotations of computational processes) and logics (lattices of properties of processes). Moreover, the underlying logic is geometric, which can be computationally interpreted as the logic of observable properties---i.e. properties which can be determined to hold of a process on the basis of a finite amount of information about its execution. These ideas lead to the following programme: 1. A metalanguage is introduced, comprising - types = universes of discourse for various computational situations. - terms = programs = syntactic intensions for models or points. 2. A standard denotational interpretation of the metalanguage is given, assigning domains to types and domain elements to terms. 3. The metalanguage is also given a {\em logical} interpretation, in which types are interpreted as propositional theories and terms are interpreted via a program logic, which axiomatizes the properties they satisfy. 4. The two interpretations are related by showing that they are Stone duals of each other. Hence, semantics and logic are guaranteed to be in harmony with each other, and in fact each determines the other up to isomorphism. This opens the way to a whole range of applications. Given a denotational description of a computational situation in our meta-language, we can turn the handle to obtain a logic for that situation.

Abstract We show that the polynomial translation of the classical propositional normal modal logic S4 into the intuitionistic propositional logic Int from Fernández is incorrect. We give a modified translation and prove its correctness, and provide implementations of both translations to allow others to test our results.

We present a labelled sequent calculus for Boolean bunched implications (BBI), a classical variant of the logic of Bunched Implications (BI). The calculus is simple, sound, complete and enjoys cut-elimination. We show that all the structural rules in the calculus, i.e. those rules that manipulate labels and ternary relations, can be localized around applications of certain logical rules, thereby localizing the handling of these rules in proof search. Based on this, we demonstrate a free variable calculus that deals with the structural rules lazily in a constraint system. We propose a heuristic method to quickly solve certain constraints, and show some experimental results to confirm that our approach is feasible for proof search. Additionally, we show that different semantics for BBI and some axioms in concrete models can be captured modularly simply by adding extra structural rules.

Abstract separation logics are a family of extensions of Hoare logic for reasoning about programs that manipulate resources such as memory locations. These logics are “abstract” because they are independent of any particular concrete resource model. Their assertion languages, called Propositional Abstract Separation Logics (PASLs), extend the logic of (Boolean) Bunched Implications (BBI) in various ways. In particular, these logics contain the connectives * and –*, denoting the composition and extension of resources, respectively. This added expressive power comes at a price, since the resulting logics are all undecidable. Given their wide applicability, even a semi-decision procedure for these logics is desirable. Although several PASLs and their relationships with BBI are discussed in the literature, the proof theory of, and automated reasoning for, these logics were open problems solved by the conference version of this article, which developed a modular proof theory for various PASLs using cut-free labelled sequent calculi. This paper non-trivially improves upon this previous work by giving a general framework of calculi on which any new axiom in the logic satisfying a certain form corresponds to an inference rule in our framework, and the completeness proof is generalised to consider such axioms. Our base calculus handles Calcagno et al.’s original logic of separation algebras by adding sound rules for partial-determinism and cancellativity, while preserving cut-elimination. We then show that many important properties in separation logic, such as indivisible unit, disjointness, splittability, and cross-split, can be expressed in our general axiom form. Thus, our framework offers inference rules and completeness for these properties for free. Finally, we show how our calculi reduce to calculi with global label substitutions, enabling more efficient implementation.

Nakano’s “later” modality, inspired by Gödel-Löb provability logic, has been applied in type systems and program logics to capture guarded recursion. Birkedal et al modelled this modality via the internal logic of the topos of trees. We show that the semantics of the propositional fragment of this logic can be given by linear converse-well-founded intuitionistic Kripke frames, so this logic is a marriage of the intuitionistic modal logic KM and the intermediate logic LC. We therefore call this logic KM lin . We give a sound and cut-free complete sequent calculus for KM lin via a strategy that decomposes implication into its static and irreflexive components. Our calculus provides deterministic and terminating backward proof-search, yields decidability of the logic and the coNP-completeness of its validity problem. Our calculus and decision procedure can be restricted to drop linearity and hence capture KM. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Abstract separation logics are a family of extensions of Hoare logic for reasoning about programs that mutate memory. These logics are "abstract" because they are independent of any particular concrete memory model. Their assertion languages, called propositional abstract separation logics, extend the logic of (Boolean) Bunched Implications (BBI) in various ways.

We propose generic declarative definitions of individual and collective trust relations between interacting agents and agent collections, and trust domains of trust-related agents in distributed systems. Our definitions yield (1) (in)compatibility, implic

Full Intuitionistic Linear Logic (FILL) is multiplicative intuitionistic linear logic extended with par. Its proof theory has been notoriously difficult to get right, and existing sequent calculi all involve inference rules with complex annotations to guarantee soundness and cut-elimination. We give a simple and annotation-free display calculus for FILL which satisfies Belnap’s generic cut-elimination theorem. To do so, our display calculus actually handles an extension of FILL, called Bi-Intuitionistic Linear Logic (BiILL), with an ‘exclusion’ connective defined via an adjunction with par. We refine our display calculus for BiILL into a cut-free nested sequent calculus with deep inference in which the explicit structural rules of the display calculus become admissible. A separation property guarantees that proofs of FILL formulae in the deep inference calculus contain no trace of exclusion. Each such rule is sound for the semantics of FILL, thus our deep inference calculus and display calculus are conservative over FILL. The deep inference calculus also enjoys the subformula property and terminating backward proof search, which gives the NP-completeness of BiILL and FILL.

We show that global caching can be used with propagation of both satisfiability and unsatisfiability in a sound manner to give an EXPTIME algorithm for checking satisfiability w.r.t. a TBox in the basic description logic ALC. Our algorithm is based on a simple traditional tableau calculus which builds an and-or graph where no two nodes of the graph contain the same formula set. When a duplicate node is about to be created, we use the pre-existing node as a proxy, even if the proxy is from a different branch of the tableau, thereby building global caching into the algorithm from the start. Doing so is important since it allows us to reason explicitly about the correctness of global caching. We then show that propagating both satisfiability and unsatisfiability via the and-or structure of the graph remains sound. In the longer paper, by combining global caching, propagation and cutoffs, our framework reduces the search space more significantly than the framework of [1]. Also, the freedom to use arbitrary search heuristics significantly increases its application potential. A longer version with all optimisations is currently under review for a journal. An extension for SHI will appear in TABLEAUX 2007.

We compare implementations of five theorem provers for Computation Tree Logic (CTL) based on tree-tableaux, graph-tableaux, binary decision diagrams, resolution and games using formula-classes from the literature. In the process, we gather and analyse a set of test formulae which could form the basis of a suite of benchmark formulae for CTL.

Bi-intuitionistic logic is the union of intuitionistic and dual intuitionistic logic, and was introduced by Rauszer as a Hilbert calculus with algebraic and Kripke semantics. But her subsequent 'cut-free' sequent calculus has recently been shown to fail cut-elimination. We present a new cut-free sequent calculus for bi-intuitionistic logic, and prove it sound and complete with respect to its Kripke semantics. Ensuring completeness is complicated by the interaction between intuitionistic implication and dual intuitionistic exclusion, similarly to future and past modalities in tense logic. Our calculus handles this interaction using derivations and refutations as first class citizens. We employ extended sequents which pass information from premises to conclusions using variables instantiated at the leaves of refutations, and rules which compose certain refutations and derivations to form derivations. Automated deduction using terminating backward search is also possible, although this is not our main purpose.

We develop clausal tableau calculi for six multimodal logics variously designed for reasoning about multi-degree belief, reasoning about distributed systems of belief and for reasoning about epistemic states of agents in multi-agent systems. Our tableau calculi are sound, complete, cut-free and have the analytic superformula property, thereby giving decision procedures for all of these logics. We also use our calculi to obtain complexity results for five of these logics. The complexity of the remaining logic was known.

We begin by showing how to faithfully encode the Classical Modal Display Logic (CMDL) of Wansing into the Calculus of Structures (CoS) of Guglielmi. Since every CMDL calculus enjoys cut-elimination, we obtain a cut-elimination theorem for all corresponding CoS calculi. We then show how our result leads to a minimal cut-free CoS calculus for modal logic S5. No other existing CoS calculi for S5 enjoy both these properties simultaneously.

1PARC, CA, USA 2ANU, Australia 3University of Bamberg, Germany

Valeria de Paiva, Rajeev Goré, Michael Mendler; Forthcoming Papers, Journal of Logic and Computation, Volume 14, Issue 4, 1 August 2004, Pages 621–622, https://

Propositional modal provability logics like G and Grz have arithmetical interpretations where □φ can be read as ‘formula φ is provable in Peano Arithmetic’. These logics are decidable but are characterized by classes of Kripke frames which are not first‐order definable. By abstracting the aspects common to their characteristic axioms we define the notion of a formula generation map F(P) in one propositional variable. We then focus our attention on the properly displayable subset of all (first‐order definable) Sahlqvist modal logics. For any logic L from this subset, we consider the (provability) logic LF obtained by the addition of an axiom based upon a formula generation map F(P) so that LF = L + F(P). The class of such logics includes G and Grz. By appropriately modifying the right introduction rules for □, we give (not necessarily cut‐free) display calculi for every such logic. We define the pseudo‐displayable subset of these logics as those whose display calculi enjoy cut‐elimination for sequents of the form ⊤ ⊢ φ for any formula φ. We then show that for any provability logic LF having a conservative tense extension, there is a map f on formulae such that LF is pseudo‐displayable if and only if f maps theorems of LF to theorems of the underlying logic L and vice versa. By using a standard renaming technique we can guarantee that there is a polynomial‐time translation from LF into L. All proofs are purely syntactic and show the versatility of display calculi since similar results using traditional Gentzen calculi are not possible for as broad a range of logics and require further conditions. Our maps generalize previously known maps from G into K4. An application of our results gives an O(n.log n)3) translation from the (‘second order’) provability logic Grz into a decidable subset of first‐order logic. Since each of our logics L is a Sahlqvist logic, it is first‐order definable, and hence each L has a translation into first‐order logic. Our results therefore show that all pseudo‐displayable logics LF are ‘essentially first‐order’ even though their characteristic axiom may not be first‐order definable.

We define display calculi for nominal tense logics extending the minimal nominal tense logic (MNTL) by addition of primitive axioms. To do so, we use the natural translation ofMNTL into the minimal tense logic of inequality (L≠) which is known to be properly displayable by application of Kracht's results. The rules of the display calculus δMNTL for MNTL mimic those of the display calculus δL≠ for L≠. We show that every MNTL‐valid formula admits a cut‐free derivation in δMNTL. We also show that a restricted display calculus δ−MNTL, is not only complete for MNTL, but that it enjoys cut‐elimination for arbitrary sequents. Finally, we give a weak Sahlqvist‐type theorem for two semantically defined extensions of MNTL. Using Kracht's techniques we obtain sound and complete display calculi for these two extensions based upon δMNTL and δ−MNTL respectively. The display calculi based upon δMNTL enjoy cut‐elimination for valid formulae only, but those based upon δ−MNTL enjoy cut‐elimination for arbitrary sequents.

We study a propositional bimodal logic consisting of two S4 modalities and [a], together with the interaction axiom scheme #a## # #a##. In the intended semantics, the plain is given the McKinsey-Tarski interpretation as the interior operator of a topology, while the labelled [a] is given the standard Kripke semantics using a reflexive and transitive binary relation Ra . The interaction axiom expresses the property that the Ra relation is lower semi-continuous with respect to the topology. The class of topological Kripke frames axiomatised by the logic includes all frames over Euclidean space where Ra is the positive flow relation of a di#erential equation. We establish the completeness of the axiomatisation with respect to the intended class of topological Kripke frames, and investigate tableau calculi for the logic, although decidability is still an open question. 1 Introduction We study a propositional bimodal logic consisting of two S4 modalities # and [a], to...

The modal logic literature is notorious for multiple axiomatizations of the same logic and for conflicting overloading of axiom names. Many of the interesting interderivability results are still scattered over the often hard to obtain classics. We catalogue the most interesting axioms, their numerous variants, and explore the relationships between them in terms of interderivability as both axiom (schema) and as simple formulae. In doing so we introduce the Logics Workbench (LWB, see http://lwbwww.uniba.ch:8080/LWBinfo.html), a versatile tool for proving theorems in numerous propositional (nonclassical) logics. As a side-effect we fulfill a call from the modal theorem proving community for a database of known theorems.

Article Automatic synthesis of Boolean equations using programmable array logic Share on Authors: R. P. Goré Dept. of Computer Science, University of Melbourne, Parkville, 3052, Australia Dept. of Computer Science, University of Melbourne, Parkville, 3052, AustraliaView Profile , K. Ramaamohanarao Dept. of Computer Science, University of Melbourne, Parkville, 3052, Australia Dept. of Computer Science, University of Melbourne, Parkville, 3052, AustraliaView Profile Authors Info & Claims DAC '89: Proceedings of the 26th ACM/IEEE Design Automation ConferenceJune 1989 Pages 283–289https://doi.org/10.1145/74382.74430Online:01 June 1989Publication History 6citation208DownloadsMetricsTotal Citations6Total Downloads208Last 12 Months3Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access