Activities such as clinical investigations (CIs) or financial processes are subject to regulations to ensure quality of results and avoid negative consequences. Regulations may be imposed by multiple governmental agencies as well as by institutional policies and protocols. Due to the complexity of both regulations and activities, there is great potential for violation due to human error, misunderstanding, or even intent. Executable formal models of regulations, protocols and activities can form the foundation for automated assistants to aid planning, monitoring and compliance checking. We propose a model based on multiset rewriting where time is discrete and is specified by timestamps attached to facts. Actions, as well as initial, goal and critical states may be constrained by means of relative time constraints. Moreover, actions may have non-deterministic effects, i.e. they may have different outcomes whenever applied. We present a formal semantics of our model based on focused proofs of linear logic with definitions. We also determine the computational complexity of various planning problems. Plan compliance problem, for example, is the problem of finding a plan that leads from an initial state to a desired goal state without reaching any undesired critical state. We consider all actions to be balanced, i.e. their pre- and post-conditions have the same number of facts. Under this assumption on actions, we show that the plan compliance problem is PSPACE-complete when all actions have only deterministic effects and is EXPTIME-complete when actions may have non-deterministic effects. Finally, we show that the restrictions on the form of actions and time constraints taken in the specification of our model are necessary for decidability of the planning problems.
In this paper, we discuss a semi-dense depth map interpolation method based on convolutional neural network. We propose a compact neural network architecture with loss function defined as Euclidean distance in the feature space of VGG-16 neural network used for deep visual recognition. The suggested solution shows state-of-art performance on synthetic and real datasets. Together with LSD-SLAM, the method could be used to provide a dense depth map for interaction purposes, such as creating a first person game in AR/MR or perception module for autonomous vehicle.
Dualization of a monotone Boolean function on a finite lattice can be represented by transforming the set of its minimal 1 values to the set of its maximal 0 values. In this paper we consider finite lattices given by ordered sets of their meet and join irreducibles (i.e., as a concept lattice of a formal context). We show that in this case dualization is equivalent to the enumeration of so-called minimal hypotheses. In contrast to usual dualization setting, where a lattice is given by the ordered set of its elements, dualization in this case is shown to be impossible in output polynomial time unless P = NP. However, if the lattice is distributive, dualization is shown to be possible in subexponential time.
Nowadays, mind mapping is rather popular educational technique. Like any other learning tools, mind maps became a part of modern educational trends like blended learning and computer-supported collaborative learning. Lots of mind mapping software tools are adopted to teaching and learning routines such as educational content delivery or assessment. This paper focuses on the additional automatic evaluation of digital educational mind maps gained from the existing procedures of assessments. The review of automatic graders which support the evaluation process demonstrates that some systematical work is done in automation grading by comparing students’ mind maps with a template. But lots of questions about automatic mind maps’ scoring by retrieving the data from a scored mind map are still open. This paper introduces the automatic grader for educational mind maps (AGEMM) which acts like a teacher’s assistant and calculates several quantitative metrics. The AGEMM is implemented as a web-service and interacted with mind maps prepared in the Coggle web-service through its API. The AGEMM is adopted to a bachelor course. Results demonstrate that scores from the AGEMM may be transformed to scales or criterial levels which are used to evaluation. Moreover, the AGEMM application revealed several problems and shew lines of development which we discuss in the paper.