Wyniki wyszukiwania - BazTech

1

Implementing Natural Language Inference for comparatives

Haruta Izumi, Mineshima Koji, Bekki Daisuke

Journal of Language Modelling

|

2022

|

Vol. 10, No.1

139--191

EN

This paper presents a computational framework for Natural Language Inference (NLI) using logic-based semantic representations and theorem-proving. We focus on logical inferences with comparatives and other related constructions in English, which are known for their structural complexity and difficulty in performing efficient reasoning. Using the so-called A-not-A analysis of comparatives, we implement a fully automated system to map various comparative constructions to semantic representations in typed first-order logic via Combinatory Categorial Grammar parsers and to prove entailment relations via a theorem prover. We evaluate the system on a variety of NLI benchmarks that contain challenging inferences, in comparison with other recent logic-based systems and neural NLI models.

2

Computing Parameterized Invariants of Parameterized Petri Nets

Esparza Javier, Raskin Mikhail, Welzel Christoph

Fundamenta Informaticae

|

2022

|

vol. 187 nr 2-4

197--243

EN

A fundamental advantage of Petri net models is the possibility to automatically compute useful system invariants from the syntax of the net. Classical techniques used for this are place invariants, P-components, siphons or traps. Recently, Bozga et al. have presented a novel technique for the parameterized verification of safety properties of systems with a ring or array architecture. They show that the statement "for every instance of the parameterized Petri net, all markings satisfying the linear invariants associated to all the P-components, siphons and traps of the instance are safe" can be encoded in WS1S and checked using tools like MONA. However, while the technique certifies that this infinite set of linear invariants extracted from P-components, siphons or traps are strong enough to prove safety, it does not return an explanation of this fact understandable by humans. We present a CEGAR loop that constructs a finite set of parameterized P-components, siphons or traps, whose infinitely many instances are strong enough to prove safety. For this we design parameterization procedures for different architectures.

3

Modeling and Verification using Different Notations for CPSs: The One-Water-Tank Case Study

Staroletov Sergey, Schulte Horst, Baar Thomas, Konyukhov Ivan, Shilov Nikolay, Rozov Andrei, Liakh Tatiana, Zyubin Vladimir

Annals of Computer Science and Information Systems

|

2021

|

Vol. 25

485--488

EN

The choice of an adequate notation and subsequent system formalization are the crucial points for the design of cyber-physical systems (CPSs). Here, an appropriate notation allows an explicit specification of the deterministic system behavior for specified initial states and inputs. We base our study on an industrial example (water tank) that comprises nominal as well as safety-critical states, and focus on the notation’s support to validate/verify crucial safety properties. Several industrial notations (e.g. Matlab/Simulink©) to design and simulate such a hybrid system have been tried based on our physical model. In addition, we remodel our example using the well-founded mathematical formalism of hybrid automata. It enables us to formally express and verify important safety properties using the theorem prover KeYmaera

4

Combining logical and distributional methods in type-logical grammars

Moot R.

Journal of Language Modelling

|

2018

|

Vol. 6, No. 2

287--317

EN

We propose a low-level way of combining distributional and logical ideas into a single formal system. This will be an instantiation of a more general system, adding weights to proof rules. These weights will not measure some sort of “confidence the proof is valid”, but Rather act as a way to prefer some proofs over others, where preference can mean “easier to process (for humans)” or “more coherent (combining words that make sense together)”. The resulting system of weighted theorem proving can be implemented either as a best-first proof serach strategy or as a polynomial-time approximation of proof search for NP-complete parsing problems.

5

Koncepcja i realizacja systemu wnioskującego Gentzena z wykorzystaniem RDBMS – IBM DB2

Gaczyński A., Tkacz J., Doligalski M.

Przegląd Elektrotechniczny

|

2012

|

R. 88, nr 8

148-151

PL

Poniższy artykuł przedstawia realizację systemu wnioskującego Gentzena z wykorzystaniem systemu zarządzania relacyjną bazą danych IBM DB2 w wersji 9.7. Niniejsza publikacja prezentuje zalety z używania procedur składowanych oraz w jaki sposób można wykorzystać strukturę tabel w bazie danych do zaawansowanego przetwarzania informacji. Przedstawia użycie bazy danych przy implementacji automatycznych systemów dowodzenia twierdzeń oraz w jaki sposób architektura klient-serwer znajduje zastosowanie w stosunku do tego typu aplikacji.

EN

The paper presents conception and design of Gentzen deduction system by using RDBMS – IBM DB2. It shows adds of stored procedures and method of using table structure in database for advanced information computing. Testing of the solution is based on the analysis of randomly generated not oriented graphs. The tests confirm the correctness of implementations, and also highlight the problem of high computational complexity. This unusual implementation and use of RDBMS environment opens up new areas of research on the optimization of reasoning algorithm.

6

Towards the Safety Verification of Real-Time Systems with the Coq Proof Assistant

Tveretina O.

Journal of Automation Mobile Robotics and Intelligent Systems

|

2009

|

Vol. 3, No. 1

30-32

EN

Hybrid systems involve the interaction of discrete and continuous dynamics. Hybrid systems have been used as a mathematical model for many safety critical applications. One of the most important analysis problems of hybrid systems is the reachability problem. In this paper we argue that the proof assistant Coq can be used for the hybrid systems verification. An example of a train crossing control is provided.

7

Towards Integrated Verification of Timed Transition Models

Lawford M., Pantelic V., Zhang H.

Fundamenta Informaticae

|

2006

|

Vol. 70, nr 1,2

75-110

EN

This paper describes an attempt to combine theorem proving and model-checking to formally verify real-time systems in a discrete time setting. The Timed Automata Modeling Environment (TAME) has been modified to provide a formal model for Time Transition Models (TTMs) in the PVS proof checker. Strong and weak state-event observation equivalences are formalized in PVS for state-event labeled transition systems (SELTS), the underlying semantic model of TTMs. The state-event equivalences form the basis of truth value preserving abstractions for a real-time temporal logic. When appropriate restrictions are placed upon the TTMs, their PVS models can be easily translated into input for the SAL model-checker. A simple real-time control system is specified and verified using these theories. While these preliminary results indicate that the combination of PVS and SAL could provide a useful environment to perform equivalence verification, model-checking and compositional model reduction of real-time systems, the current implementation in the general purpose SAL model-checker lags well behind state of the art real-time model-checkers.

8

The Complexity of Equitable Vertex Coloring of Graphs

Furmańczyk H., Kubale M.

Journal of Applied Computer Science

|

2005

|

Vol. 13, nr 2

95-106

EN

A graph is equitably k-colorable if its vertices can be partitioned into k independent sets in such a way that the number of vertices in any two sets differ by at most one. The smallest k for which such a coloring exists is known as the equitable chromatic number of G and denoted by X=(G). In the paper we give formulas for the equitable chromatic number of some highly-structured graphs and some graph products. We present also two polynomial-time algorithms for equitable graph coloring with suboptimal number of colors.

9

Intelligible Automated Reasoning: Systems with the Resolution, Induction and Symmetry

Poliscuk J.E.

Journal of Applied Computer Science

|

2005

|

Vol. 13, nr 2

7-28

EN

In mathematics, the programs for proving theorems could be instruments for testing the existing proofs and can be used to test hypotheses, and the programs which allow man’s influence on the process of proving could be used to prove new theorems. An independent theoretical contribution is made by the discovery of the adequate rules of deduction and the automatic procedures for proving. The paper presents a short version of the fully automated programmed systems, intended for proving of theorems in the first-order predicate calculus. Proofs in the form of refutations are based on the following rules of derivation: the orderly linear resolution with marked literals (OL- resolution), the rules of binary induction (Prule) and the rules of symmetry.

10

Data Mining-Based Intelligent Equipment Maintenance System in Telecommunication Network

Sodiya A. S., Longe H. O. D., Ibrahim S. A.

Journal of Applied Computer Science

|

2005

|

Vol. 13, nr 2

29-38

EN

The concept of data mining, which has become a promising field because of its applications in various fields, is used in this work for strategic equipment maintenance in telecommunication network. Efficient maintenance of equipment in large telecommunication networks is difficult and complex. Thus, there is need for intelligent systems to guide engineers in proper maintenance of equipment in telecommunication network installations. The idea is to apply modified Apriori frequent pattern algorithm to mine frequent faulty events and identity association rules among items in telecommunication network alarm database. We implemented the novel approach on faulty events database of a GSM company in Nigeria. The result shows a promising tool that is much needed for intelligent decision-making in equipment maintenance in telecommunication installations.

11

Automating inductive specification proofs

Pientka B., Kreitz Ch.

Fundamenta Informaticae

|

1999

|

Vol. 39, Nr 1,2

189-209

EN

We present an automatic method which combines logical proof search and rippling heuristics to prove specifications. The key idea is to instantiate meta-variables in the proof with a simultaneous match based on rippling/reverse rippling heuristic. Underlying our rippling strategy is the rippling distance strategy which introduces a new powerful approach to rippling, as it avoids termination problems of other rippling strategies. Moreover, we are able to synthesize conditional substitutions for meta-variables in the proof. The strength of our approach is illustrated by discussing the specification of the integer square root and automatically synthesizing the corresponding algorithm. The described procedure has been integrated as a tactic into the NUPRL system but it can be combined with other proof methods as well.

12

Automated deduction techniques for studying Rough Algebras

Vigneron L.

Fundamenta Informaticae

|

1998

|

Vol. 33, nr 1

85-103

EN

We present a non-exhaustive state of the art. In the domain of deduction in first-order logic with equality, describing different strategies introduced over the years: strategies for selecting deduction steps, for eliminating redundant information, for delaying the resolution of unsolved or too difficult problems, for applying deductions with built-in-properties. We also present the system dalac that implements our deduction techniques modulo associative-commutative properties. Finally we detail an application of those techniques to the study of non-classical logics, work realised in collaboration with Prof. Wasilewska (Stony Brook University, New York).