Results 11 to 20 of about 9,301 (306)
Proof-relevant pi-calculus [PDF]
Electronic Proceedings in Theoretical Computer Science, 2015 Formalising the pi-calculus is an illuminating test of the expressiveness of logical frameworks and mechanised metatheory systems, because of the presence of name binding, labelled transitions with name extrusion, bisimulation, and structural congruence.
Roly Perera, James Cheney
doaj +7 more sources
Proof nets for the Displacement calculus [PDF]
, 2016 We present a proof net calculus for the Displacement calculus and show its correctness. This is the first proof net calculus which models the Displacement calculus directly and not by some sort of translation into another formalism. The proof net calculus opens up new possibilities for parsing and proof search with the Displacement calculus.
Richard Moot
openalex +5 more sources
A new proof of the generalized Hamiltonian–Real calculus [PDF]
Royal Society Open Science, 2016 The recently introduced generalized Hamiltonian–Real (GHR) calculus comprises, for the first time, the product and chain rules that makes it a powerful tool for quaternion-based optimization and adaptive signal processing.
Dongpo Xu, Hua Gao, Danilo P. Mandic
doaj +2 more sources
A labelled sequent calculus for BBI: proof theory and proof search [PDF]
Journal of Logic and Computation, 2015 We present a labelled sequent calculus for Boolean BI, a classical variant of O'Hearn and Pym's logic of Bunched Implication. The calculus is simple, sound, complete, and enjoys cut-elimination. We show that all the structural rules in our proof system, including those rules that manipulate labels, can be localised around applications of certain ...
Zhé Hóu, Rajeev Goré, Alwen Tiu
openalex +6 more sources
Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search [PDF]
Mathematical Structures in Computer Science, 2019 A new approach to inhabitation problems in simply typed lambda-calculus is shown, dealing with both decision and counting problems. This approach works by exploiting a representation of the search space generated by a given inhabitation problem, which is in terms of a lambda-calculus for proof search that the authors developed recently.
José Espírito Santo +2 more
+10 more sources
Proof nets and the call-by-value λ-calculus [PDF]
Electronic Proceedings in Theoretical Computer Science, 2015 In Proceedings LSFA 2012, arXiv:1303 ...
Beniamino Accattoli
openalex +6 more sources
Cyclic proofs for the first-order µ-calculus
Logic Journal of the IGPL, 2022 Abstract We introduce a path-based cyclic proof system for first-order $\mu $-calculus, the extension of first-order logic by second-order quantifiers for least and greatest fixed points of definable monotone functions. We prove soundness of the system and demonstrate it to be as expressive as the known trace-based cyclic systems of Dam ...
Bahareh Afshari +2 more
openalex +4 more sources
A Calculus of Circular Proofs and its Categorical Semantics [PDF]
BRICS Report Series, 2001 <p>We present a calculus of proofs, the intended models of which<br />are categories with finite products and coproducts, initial algebras<br />and final coalgebras of functors that are recursively constructible<br />out of these operations, that is, mu-bicomplete categories.
Luigi Santocanale
openalex +3 more sources
A new graphical calculus of proofs [PDF]
Electronic Proceedings in Theoretical Computer Science, 2011 We offer a simple graphical representation for proofs of intuitionistic logic, which is inspired by proof nets and interaction nets (two formalisms originating in linear logic).
Sandra Alves +2 more
doaj +4 more sources
A Finite-Model-Theoretic View on Propositional Proof Complexity [PDF]
Logical Methods in Computer Science, 2022 We establish new, and surprisingly tight, connections between propositional proof complexity and finite model theory. Specifically, we show that the power of several propositional proof systems, such as Horn resolution, bounded-width resolution, and the ...
Erich Grädel +3 more
doaj +1 more source