the classical Floyd-Hoare logic is defined for the case of total pre- and postconditions and partial programs (i.e. programs can be undefined on some input data, but conditions must be defined on all data). In this pa...
详细信息
ISBN:
(纸本)9783319761688
the classical Floyd-Hoare logic is defined for the case of total pre- and postconditions and partial programs (i.e. programs can be undefined on some input data, but conditions must be defined on all data). In this paper we propose an extension of this logic for the case of partial conditions and partial programs over structured data. these data are based on two constructing primitives: naming and relational structuring and are called relational nominative data. they can conveniently represent many data structures used in programming. the semantics of the proposed logic is represented by special algebras of partial functions and predicates over relational nominative data. Operations of these algebras are called compositions. We present an inference system for the mentioned logic and propose an approach to its formalization in Mizar proof assistant. the obtained results can be used in software verification.
the theta-subsumption test is known to be a bottleneck in inductivelogicprogramming. the state-of-the-art learning systems in this field are hardly scalable. Last year, we have created a distributed theta-subsumptio...
详细信息
the theta-subsumption test is known to be a bottleneck in inductivelogicprogramming. the state-of-the-art learning systems in this field are hardly scalable. Last year, we have created a distributed theta-subsumption process based on an Actor Model, withthe aim of being able to decide subsumption on very large clauses. this model was correct and complete, but was also very slow. this is why we introduce ANTS (Actor Network based theta-Subsumption), a new model also based on an actor network, which is significantly faster than the previous one.
Answer Set programming (ASP) is a well-known paradigm of declarative programming with roots in logicprogramming and non-monotonic reasoning. Similar to other closely related problem-solving technologies, such as SAT/...
详细信息
Answer Set programming (ASP) is a well-known paradigm of declarative programming with roots in logicprogramming and non-monotonic reasoning. Similar to other closely related problem-solving technologies, such as SAT/SMT, QBF, Planning and Scheduling, advancements in ASP solving are assessed in competition events. In this paper, we report about the design and results of the Sixth ASP Competition, which was jointly organized by the University of Calabria (Italy), Aalto University (Finland), and the University of Genoa (Italy), in affiliation withthe 13thinternationalconference on logicprogramming and Non-Monotonic Reasoning. this edition maintained some of the design decisions introduced in 2014, e.g., the conception of sub-tracks, the scoring scheme, and the adherence to a fixed modeling language in order to push the adoption of the ASP-Core-2 standard. On the other hand, it featured also some novelties, like a benchmark selection stage classifying instances according to their empirical hardness, and a "Marathon" track where the top-performing systems are given more time for solving hard benchmarks.
TEMPLATE-COQ (https://***/template-coq) is a plugin for COQ, originally implemented by Malecha [18], which provides a reifier for COQ terms and global declarations , as represented in the COQ kernel, as well as a deno...
详细信息
ISBN:
(数字)9783319948218
ISBN:
(纸本)9783319948218;9783319948201
TEMPLATE-COQ (https://***/template-coq) is a plugin for COQ, originally implemented by Malecha [18], which provides a reifier for COQ terms and global declarations , as represented in the COQ kernel, as well as a denotation command. Initially, it was developed for the purpose of writing functions on COQ's AST in GAL-LINA. Recently, it was used in the CERTICOQ certified compiler project [4], as its front-end language, to derive parametricity properties [3], and to extract COQ terms to a CBV lambda-calculus [13]. However, the syntax lacked semantics, be it typing semantics or operational semantics, which should reflect, as formal specifications in COQ, the semantics of COQ's type theory itself. the tool was also rather bare bones, providing only rudimentary quoting and unquoting commands. We generalize it to handle the entire Calculus of inductive Constructions (CIC), as implemented by COQ, including the kernel's declaration structures for definitions and inductives, and implement a monad for general manipulation of COQ'S logical environment. We demonstrate how this setup allows COQ users to define many kinds of general purpose plugins, whose correctness can be readily proved in the system itself, and that can be run efficiently after extraction. We give a few examples of implemented plugins, including a parametricity translation. We also advocate the use of TEMPLATE-COQ as a foundation for higher-level tools.
the problem of video monitoring of laboratory rodents by the means of object-oriented logicprogramming is considered. the videos are produced in neurophysiological experiments on the study of convulsive electrical ac...
详细信息
ISBN:
(纸本)9781538642832
the problem of video monitoring of laboratory rodents by the means of object-oriented logicprogramming is considered. the videos are produced in neurophysiological experiments on the study of convulsive electrical activity of the brain cortex. Videos of behaviour of laboratory rats were recorded simultaneously with electroencephalograms (EEG) in the animals. A comparison of EEG data withthe behaviour of the animals is necessary because sharp motions of the animals can result in EEG signals that are very similar to the epileptic discharges. thus, the first task of the video monitoring is recognition of the sharp motions of the animals and using this information for proper interpretation of the results of the experiments. the second task of the video monitoring is analysis of behaviour of animals in cognitive testing. Essential feature of the video records is in that the experiments are conducted in the same cage where the animal lives, that is, the background of the cage is sawdust. the colour of the animals is about the same as the colour of the sawdust;thus the detection of the animals is not a simple task. In the paper, development of low-level algorithms for video analysis as well as logical methods for the analysis of the animal behaviour is discussed. the methods and algorithms are implemented in the Actor Prolog object-oriented logic language.
the Θ-subsumption test is known to be a bottleneck in inductivelogicprogramming. the state-of-the-art learning systems in this field are hardly scalable. So we introduce a new Θ-subsumption algorithm based on an A...
详细信息
the Θ-subsumption test is known to be a bottleneck in inductivelogicprogramming. the state-of-the-art learning systems in this field are hardly scalable. So we introduce a new Θ-subsumption algorithm based on an Actor Model, withthe aim of being able to decide subsumption on very large clauses. We use Akka, a powerful tool to build distributed actor systems based on the JVM and the Scala language.
Uncertain single machine scheduling problem for batches of jobs is an important issue for manufacturing systems. In this paper, we use uncertainty theory to study the single machine scheduling problem with deadlines w...
详细信息
Uncertain single machine scheduling problem for batches of jobs is an important issue for manufacturing systems. In this paper, we use uncertainty theory to study the single machine scheduling problem with deadlines where the processing times are described by uncertain variables with known uncertainty distributions. A new model for this problem is built to maximize expected total weight of batches of jobs. then the model is transformed into a deterministic integer programming model by using the operational law for inverse uncertainty distributions. In addition, a property of the transformed model is provided and an algorithm is designed to solve this problem. Finally, a numerical example is given to illustrate the effectiveness of the model and the proposed algorithm.
Statistical Relational Learning (SRL) approaches have been developed to learn in presence of noisy relational data by combining probability theory with first order logic. While powerful, most learning approaches for t...
详细信息
Industrial control system failures can be hazardous to human lives and the environment. Programmable logic controllers are major components of industrial control systems that are used across the critical infrastructur...
详细信息
ISBN:
(纸本)9783319672083;9783319672076
Industrial control system failures can be hazardous to human lives and the environment. Programmable logic controllers are major components of industrial control systems that are used across the critical infrastructure. Attack and accident investigations involving programmable logic controllers rely on forensic techniques to establish the root causes and to develop mitigation strategies. However, programmable logic controller forensics is a challenging task, primarily because of the lack of system logging. this chapter proposes a novel methodology that logs the values of relevant memory addresses used by a programmable logic controller program along withtheir timestamps. Machine learning techniques are applied to the logged data to identify anomalous or abnormal programmable logic controller operations. An application of the methodology to a simulated traffic light control system demonstrates its effectiveness in performing forensic investigations of programmable logic controllers.
the classical Floyd-Hoare logic is defined for the case of total pre- and postconditions and partial programs (i.e. programs can be undefined on some input data, but conditions must be defined on all data). In this pa...
详细信息
the classical Floyd-Hoare logic is defined for the case of total pre- and postconditions and partial programs (i.e. programs can be undefined on some input data, but conditions must be defined on all data). In this paper we propose an extension of this logic for the case of partial conditions and partial programs on hierarchically organized data. these data are based on the naming relation and are called nominative data. they can conveniently represent many data structures used in programming. the semantics of the proposed logic is represented by special algebras of partial functions and predicates over nominative data. Operations of these algebras are called compositions. We present an inference system for the mentioned logic and propose an approach to its formalization in Mizar proof assistant. the obtained results can be used in software verification.
暂无评论