Sciweavers

CSFW
2012
IEEE
11 years 11 months ago
Labeled Sequent Calculi for Access Control Logics: Countermodels, Saturation and Abduction
—We show that Kripke semantics of modal logic, manifest in the syntactic proof formalism of labeled sequent calculi, can be used to solve three central problems in access control...
Valerio Genovese, Deepak Garg, Daniele Rispoli
FOSSACS
2012
Springer
12 years 5 months ago
Functions as Session-Typed Processes
We study type-directed encodings of the simply-typed λ-calculus in a session-typed π-calculus. The translations proceed in two steps: standard embeddings of simply-typed λ-calcu...
Bernardo Toninho, Luís Caires, Frank Pfenni...
SLOGICA
2010
135views more  SLOGICA 2010»
13 years 4 months ago
A Contraction-free and Cut-free Sequent Calculus for Propositional Dynamic Logic
In this paper we present a sequent calculus for propositional dynamic logic built using an enriched version of the tree-hypersequent method and including an infinitary rule for the...
Brian Hill, Francesca Poggiolesi
APAL
2011
13 years 4 months ago
A sorting network in bounded arithmetic
We formalize the construction of Paterson’s variant of the Ajtai–Koml´os–Szemer´edi sorting network of logarithmic depth in the bounded arithmetical theory VNC1 ∗ (an ex...
Emil Jerábek
CORR
2010
Springer
194views Education» more  CORR 2010»
13 years 6 months ago
A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems
Basic proof search tactics in logic and type theory can be seen as the root-rst applications of rules in an appropriate sequent calculus, preferably without the redundancies gener...
Stéphane Lengrand, Roy Dyckhoff, James McKi...
CORR
2010
Springer
155views Education» more  CORR 2010»
13 years 6 months ago
A Proof Theoretic Analysis of Intruder Theories
We consider the problem of intruder deduction in security protocol analysis: that is, deciding whether a given message M can be deduced from a set of messages under the theory of ...
Alwen Tiu, Rajeev Goré, Jeremy E. Dawson
LOGCOM
2010
136views more  LOGCOM 2010»
13 years 7 months ago
Combining Derivations and Refutations for Cut-free Completeness in Bi-intuitionistic Logic
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 ...
Rajeev Goré, Linda Postniece
IANDC
2010
141views more  IANDC 2010»
13 years 8 months ago
Regaining cut admissibility in deduction modulo using abstract completion
stract Completion Guillaume Burel a,c,∗ Claude Kirchner b,c aNancy-Universit´e, Universit´e Henri Poincar´e bINRIA Bordeaux - Sud-Ouest cLORIA, ´Equipe Pareo, Bˆatiment B, C...
Guillaume Burel, Claude Kirchner
LOGCOM
1998
110views more  LOGCOM 1998»
13 years 9 months ago
leanTAP Revisited
A sequent calculus of a new sort is extracted from the Prolog program leanTAP. This calculus is sound and complete, even though it lacks almost all structural rules. Thinking of l...
Melvin Fitting
CORR
1999
Springer
75views Education» more  CORR 1999»
13 years 9 months ago
A System of Interaction and Structure
This paper introduces a logical system, called BV , which extends multiplicative linear logic by a non-commutative self-dual logical operator. This extension is particularly challe...
Alessio Guglielmi