The CCIS series is devoted to the publication of proceedings of computer science conferences. Its aim is to efficiently disseminate original research results in informatics in printed and electronic form. While the focus is on publication of peer-reviewed full papers presenting mature work, inclusion of reviewed short papers reporting on work in progress is welcome, too. Besides globally relevant meetings with internationally representative program committees guaranteeing a strict peer-reviewing and paper selection process, conferences run by societies or of high regional or national relevance are also considered for publication.
The article discusses issues related to computer science and programming teaching for undergraduate students of universities and collegues. Enrollee's classification and expected learning outcomes are included. Every discipline included in Computer Science course is also described in details
The Formal Grammar conference series (FG) provides a forum for the presentation of new and original research on formal grammar, mathematical linguistics, and the application of formal and mathematical methods to the study of natural language. Themes of interest include, but are not limited to: – Formal and computational phonology, morphology, syntax, semantics, and pragmatics – Model-theoretic and proof-theoretic methods in linguistics – Logical aspects of linguistic structure – Constraint-based and resource-sensitive approaches to grammar – Learnability of formal grammar – Integration of stochastic and symbolic models of grammar – Foundational, methodological, and architectural issues in grammar and linguistics – Mathematical foundations of statistical approaches to linguistic analysis Previous FG meetings were held in Barcelona (1995), Prague (1996), Aix-en-Provence (1997), Saarbrücken (1998), Utrecht (1999), Helsinki (2001), Trento (2002), Vienna (2003), Nancy (2004), Edinburgh (2005), Malaga (2006), Dublin (2007), Hamburg (2008), Bordeaux (2009), Copenhagen (2010), Ljubljana (2011), Opole (2012), Düsseldorf (2013), Tübingen (2014), Barcelona (2015), Bolzano-Bozen (2016), and Toulouse (2017). FG 2018, the 23rd conference on Formal Grammar, was held in Sofia, Bulgaria, during August 11–12, 2018. The conference consisted in a special session, dedicated to the memory of Richard T. Oehrle, who passed away in 2018, and seven contributed papers selected from 11 submissions. The present volume includes the contributed papers. We would like to thank the people who made the 23rd FG conference possible: the invited speakers, the members of the Program Committee, and the organizers of ESSLLI 2018, with which the conference was colocated. August 2018 Annie Foret Gerg Kobele Sylvain Pogodalla
In their seminal paper:
Lincoln, P., Mitchell, J., Scedrov, A. and Shankar, N. (1992). Decision problems for propositional linear logic. Annals of Pure and Applied Logic 56 (1–3) 239–311,
LMSS have established an extremely surprising result that propositional linear logic is undecidable. Their proof is very complex and involves numerous nested inductions of different kinds. Later an alternative proof for the LL undecidability has been developed based on simulation Minsky machines in linear logic: Kanovich, M. (1995). The direct simulation of Minsky machines in linear logic. In: Girard, J.-Y., Lafont, Y. and Regnier, L. (eds.) Advances in Linear Logic, London Mathematical Society Lecture Notes, volume 222, Cambridge University Press 123–145. Notice that this direct simulation approach has been successfully applied for a large number of formal systems with resolving a number of open problems in computer science and even computational linguistics, e.g.,
James Brotherston, Max I. Kanovich: Undecidability of Propositional Separation Logic and Its Neighbours. J. ACM 61(2): 14:1-14:43 (2014), Max Kanovich, Stepan Kuznetsov, Andre Scedrov: Undecidability of the Lambek Calculus with a Relevant Modality. FG 2016: 240-256. Nevertheless, recently the undecidability of linear logic is questioned by some people. They claim that they have found lacunae in the LMSS 1992 paper, and, moreover, they have a proof that propositional linear logic is decidable!!! I have been asked to submit a paper, as clear as possible, to the Journal, in order to sort out such a confusing problem, once and for all.
Here, we give a fully self-contained, easy-to-follow, but fully detailed, direct and constructive proof of the undecidability of a very simple Horn-like fragment of linear logic, the proof is accessible to a wide range of people. Namely, we show that there is a direct correspondence between terminated computations of a Minsky machine M and cut-free linear logic derivations for a Horn-like sequent of the form \Phi_M, l1 |- l0 where \Phi_M consists only of Horn-like implications of the very simple forms. Neither negation, nor &, nor constants, nor embedded implications/bangs are used here. Furthermore, our particular correspondence constructed above provides decidability for some smaller Horn-like fragments along with the complexity bounds that come from the proof.
Logical frameworks allow the specification of deductive systems using the same logical machinery. Linear logical frameworks have been successfully used for the specification of a number of computational, logics and proof systems. Its success relies on the fact that formulas can be distinguished as linear, which behave intuitively as resources, and unbounded, which behave intuitionistically. Commutative subexponentials enhance the expressiveness of linear logic frameworks by allowing the distinction of multiple contexts. These contexts may behave as multisets of formulas or sets of formulas. Motivated by applications in distributed systems and in type-logical grammar, we propose a linear logical framework containing both commutative and non-commutative subexponentials. Non-commutative subexponentials can be used to specify contexts which behave as lists, not multisets, of formulas. In addition, motivated by our applications in type-logical grammar, where the weakenening rule is disallowed, we investigate the proof theory of formulas that can only contract, but not weaken. In fact, our contraction is non-local. We demonstrate that under some conditions such formulas may be treated as unbounded formulas, which behave intuitionistically.