A5013433601- Logic, programming, and type systems
- Logic, Reasoning, and Knowledge
- Distributed and Parallel Computing Systems
- Formal Methods in Verification
- Economic and Technological Developments in Russia
- Ocean Waves and Remote Sensing
- Aquatic and Environmental Studies
- Advanced Data Processing Techniques
- Advanced Data Storage Technologies
- Cloud Computing and Resource Management
- Ship Hydrodynamics and Maneuverability
- Graph Theory and Algorithms
- Oceanographic and Atmospheric Processes
- Parallel Computing and Optimization Techniques
- Advanced Algebra and Logic
- Advanced Database Systems and Queries
- Maritime Navigation and Safety
- Semantic Web and Ontologies
- Particle Accelerators and Free-Electron Lasers
- Arctic and Antarctic ice dynamics
- Security and Verification in Computing
- Scientific Computing and Data Management
- Laser Design and Applications
- Cognitive Computing and Networks
- Distributed systems and fault tolerance
St Petersburg University
2014-2024
V. N. Karazin Kharkiv National University
2024
Moscow Institute of Physics and Technology
2021-2023
Plekhanov Russian University of Economics
2020-2021
Joint Institute for Nuclear Research
2021
Marine Hydrophysical Institute
2018
King's College London
2003-2015
Ufa State Aviation Technical University
2014
King's College Hospital
2003-2006
Taras Shevchenko National University of Kyiv
1993-2005
Until recently, First-Order Temporal Logic (FOTL) has been only partially understood. While it is well known that the full logic no finite axiomatisation, a more detailed analysis of fragments was not previously available. However, breakthrough by Hodkinson et al., identifying finitely axiomatisable fragment, termed monodic led to improved understanding FOTL. Yet, in order utilise these theoretical advances, important have appropriate proof techniques for this fragment.In paper, we modify...
Virtual private supercomputer is an efficient way of conducting experiments on high-performance computational environment and the main role in this approach played by virtualization data consolidation. During experiment used to abstract application from underlying hardware also operating system offering consistent API for distributed computations. In between consolidation store initial results a storage offers processing. Combined, these APIs form solid basis shifting user focus...
The problem of wave climate description and modeling are considered on both a short-term synoptic basis. is as an ensemble conditions spatio-temporal fields characterized by frequency-directional spectra. Using expanded set wind characteristics makes it possible to correctly introduce the concept weather “scenario” use evaluate vessel safety. mathematical basis representation stochastic processes generalized autoregressive model (ARM) related models periodically correlated random process. An...
The notion of simultaneous rigid E-unification was introduced in 1987 the area automated theorem proving with equality sequent-based methods, for example connection method or tableau method. Recently, shown undecidable. Despite importance this notion, intuitionistic logic, very little is known its decidable fragments. We prove decidability results fragments monadic and show connections between some algorithmic problems logic computer science.
We develop a constraint-based technique which allows one to prove decidability and complexity results for sequent calculi. Specifically, we study problems the prenex fragment of intuitionistic logic. introduce an analogue Skolemization logic with equality, PSPACE-completeness two fragments without equality some other results. In proofs, use combination techniques constraint satisfaction, loop-free systems properties simultaneous rigid E-unification.
First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science Artificial Intelligence. While the full highly complex, recent work on monodic first-order logics has identified important enumerable even decidable fragments. In this paper, we develop clausal resolution method for fragment of over expanding domains. We first define normal form formulae then introduce novel calculi that can be applied to form. state correctness...
The paper is dedicated to the potential application of grid technology for modeling spatial- temporal wave and wind field characteristics (wave climate modeling). With reference shipbuilding knowledge necessary while ship engineering offshore construction development operation. Software complex calculations represents a set physical- mathematical models, describing frequency- directional spectra, including input meteorological data pre-processing post-processing output data. distributed...