Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 9

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
Wyszukiwano:
w słowach kluczowych:  theorem proving
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
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.
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.
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.
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.
5
Content available remote The Complexity of Equitable Vertex Coloring of Graphs
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.
6
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.
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.
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.
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).
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.