19.11.2018 14:00 @ Hora Informaticae
We present a technique describing how to effectively train a neural network given an image to produce a formal description of the given image. The basic motivation of the proposed technique is an intention to design a new tool for automatic program synthesis capable of transforming sensory data (in our case static image, but generally a "phenotype") to a formal code expression (i.e. syntactic tree of a program), such that the code (from evolutionary perspective a "genotype") evaluates to a value that is similar to the input data, ideally identical. Our approach is partially based on our technique for generating program expressions in the context of typed functional genetic programming. We present promising results evaluating a simple image description language achieved with a deep network combining convolution encoder of images and recurrent decoder for generating program expressions in the sequential prefix notation and propose possible future applications.
21.11.2018 16:00 @ Applied Mathematical Logic
Frame semantics, given by Kripke or neighborhood frames, do not give completeness theorems for all modal logics extending, respectively, K and E. Such shortcoming can be overcome by means of general frames, i.e. frames equipped with a collection of admissible sets of worlds (which is the range of possible valuations over such frame). We export this approach from the classical paradigm to modal many-valued logics by defining general A-frames over a given residuated lattice A (i.e., the usual frames with a collection of admissible A-valued sets). We describe in details the relation between general Kripke and neighborhood A-frames and prove that, if the logic of A is finitary, all extensions of the corresponding logic E of A are complete w.r.t. general neighborhood frames. Our work provides a new approach to the current research trend of generalizing relations semantics for non-classical modal logics to circumvent axiomatization problems.
28.11.2018 16:00 @ Applied Mathematical Logic
While the relations between an operation and its residuals play an essential role in substructural logic, a closely related relation between operations is that of conjugation - so closely related that with Boolean negation, the conjugates and residuals of an operation are interde_nable. In this talk extensions of the Lambek Calculus including conjugates of fusion (without negation) are investigated. Some interesting properties of the conjugates are discussed, a proof system is presented, its adequacy questioned, and some applications are considered.