← Publications (abstracts)

[1]

Bobot, F., and Paskevich, A. Expressing polymorphic types in a many-sorted language. In FroCoS 2011, 8th International Symposium on Frontiers of Combining Systems (Saarbrücken, Germany, Oct. 2011), C. Tinelli and V. Sofronie-Stokkermans, Eds., vol. 6989 of Lecture Notes in Computer Science, Springer, pp. 87-102. [ bib | .pdf ]

In this paper, we study translation from a first-order logic with polymorphic types à la ML (of which we give a formal description) to a many-sorted or one-sorted logic as accepted by mainstream automated theorem provers. We consider a three-stage scheme where the last stage eliminates polymorphic types while adding the necessary "annotations" to preserve soundness, and the first two stages serve to protect certain terms so that they can keep their original unannotated form. This protection allows us to make use of provers' built-in theories and operations. We present two existing translation procedures as sound and complete instances of this generic scheme. Our formulation generalizes over the previous ones by allowing us to protect terms of arbitrary monomorphic types. In particular, we can benefit from the built-in theory of arrays in SMT solvers such as Z3, CVC3, and Yices. The proposed methods are implemented in the Why3 tool and we compare their performance in combination with several automated provers.

[2]

Bobot, F., and Paskevich, A. Expressing polymorphic types in a many-sorted language, July 2011. Extended report. [ bib | http | .pdf ]

In this paper, we study translation from a first-order logic with polymorphic types à la ML (of which we give a formal description) to a many-sorted or one-sorted logic as accepted by mainstream automated theorem provers. We consider a three-stage scheme where the last stage eliminates polymorphic types while adding the necessary "annotations" to preserve soundness, and the first two stages serve to protect certain terms so that they can keep their original unannotated form. This protection allows us to make use of provers' built-in theories and operations. We present two existing translation procedures as sound and complete instances of this generic scheme. Our formulation generalizes over the previous ones by allowing us to protect terms of arbitrary monomorphic types. In particular, we can benefit from the built-in theory of arrays in SMT solvers such as Z3, CVC3, and Yices. The proposed methods are implemented in the Why3 tool and we compare their performance in combination with several automated provers.

[3]

Bobot, F., Filliâtre, J.-C., Marché, C., and Paskevich, A. Why3: Shepherd your herd of provers. In Boogie 2011, First International Workshop on Intermediate Verification Languages (Wrocław, Poland, Aug. 2011), pp. 53-64. [ bib | .pdf ]

Why3 is the next generation of the Why software verification platform. Why3 clearly separates the purely logical specification part from generation of verification conditions for programs. This article focuses on the former part. Why3 comes with a new enhanced language of logical specification. It features a rich library of proof task transformations that can be chained to produce a suitable input for a large set of theorem provers, including SMT solvers, TPTP provers, as well as interactive proof assistants.

[4]

Contejean, É., Courtieu, P., Forest, J., Paskevich, A., Pons, O., and Urbain, X. A3PAT, an approach for certified automated termination proofs. In PEPM'10, Proceedings of the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (Madrid, Spain, Jan. 2010), ACM, pp. 63-72. [ bib | DOI | .pdf ]

Software engineering, automated reasoning, rule-based programming or specifications often use rewriting systems for which termination, among other properties, may have to be ensured.This paper presents the approach developed in Project A3PAT to discover and moreover certify, with full automation, termination proofs for term rewriting systems.

It consists of two developments: the Coccinelle library formalises numerous rewriting techniques and termination criteria for the Coq proof assistant; the CiME3 rewriting tool translates termination proofs (discovered by itself or other tools) into traces that are certified by Coq assisted by Coccinelle.

The abstraction level of our formalisation allowed us to weaken premises of some theorems known in the literature, thus yielding new termination criteria, such as an extension of the powerful subterm criterion (for which we propose the first full Coq formalisation). Techniques employed in CiME3 also improve on previous works on formalisation and analysis of dependency graphs.

[5]

Verchinine, K., Lyaletski, A., Paskevich, A., and Anisimov, A. On correctness of mathematical texts from a logical and practical point of view. In Intelligent Computer Mathematics, AISC/Calculemus/MKM 2008 (Birmingham, United Kingdom, July 2008), S. Autexier, J. Campbell, J. Rubio, V. Sorge, M. Suzuki, and F. Wiedijk, Eds., vol. 5144 of Lecture Notes in Computer Science, Springer, pp. 583-598. [ bib | .pdf ]

Formalizing mathematical argument is a fascinating activity in itself and (we hope!) also bears important practical applications. While traditional proof theory investigates deducibility of an individual statement from a collection of premises, a mathematical proof, with its structure and continuity, can hardly be presented as a single sequent or a set of logical formulas. What is called “mathematical text”, as used in mathematical practice through the ages, seems to be more appropriate. However, no commonly adopted formal notion of mathematical text has emerged so far.

In this paper, we propose a formalism which aims to reflect natural (human) style and structure of mathematical argument, yet to be appropriate for automated processing: principally, verification of its correctness (we consciously use the word rather than “soundness” or “validity”).

We consider mathematical texts that are formalized in the ForTheL language (brief description of which is also given) and we formulate a point of view on what a correct mathematical text might be. Logical notion of correctness is formalized with the help of a calculus. Practically, these ideas, methods and algorithms are implemented in a proof assistant called SAD. We give a short description of SAD and a series of examples showing what can be done with it.

[6]

Paskevich, A. Connection tableaux with lazy paramodulation. Journal of Automated Reasoning 40, 2-3 (2008), 179-194. [ bib | .pdf ]

It is well known that the connection refinement of clause tableaux with paramodulation is incomplete (even with weak connections). In this paper, we present a new connection tableau calculus for logic with equality. This calculus is based on a lazy form of paramodulation where parts of the unification step become auxiliary subgoals in a tableau and may be subjected to subsequent paramodulations. Our calculus uses ordering constraints and a certain form of the basicness restriction.

[7]

Paskevych, A. Méthodes de formalisation des connaissances et des raisonnements mathématiques: aspects appliqués et théoriques. PhD thesis, Université Paris 12, 2007. In French. [ bib | .pdf ]

We study the means of presentation of mathematical knowledge and reasoning schemes. Our research aims at an automated system for verification of formalized mathematical texts.

In this system, a text to verify is written in a formal language which is close to the natural language and style of mathematical publications. Our intention is to exploit the hint which are given to us by the «human» form of the problem: definitions, proof schemes, nouns denoting classes of objects, etc. We describe such a language, called ForTheL.

Verification consists in showing that the text is «sensible» and «grounded», that functions and relations are applied within the domain, according to the definitions, and assertions follow from their respective premises. A formal definition of a correct text relies on a sound sequent calculus and on the notion of local validity (local with respect to some occurrence inside a formula).

Proof search is carried out on two levels. The lower level is an automated theorem prover based on a combinatorial procedure. We introduce a variant of connection tableaux which is sound and complete in the first-order logic with equality.

The higher level is a «reasoner» which employs natural proving techniques in order to filter, simplify, decompose a proof task before passing it to the prover. The algorithms of the reasoner are based on transformations that preserve the locally valid propositions.

The proposed methods are implemented in the proof assistant SAD.

[8]

Paskevich, A., Verchinine, K., Lyaletski, A., and Anisimov, A. Reasoning inside a formula and ontological correctness of a formal mathematical text. In Calculemus/MKM 2007 - Work in Progress (Hagenberg, Austria, June 2007), M. Kauers, M. Kerber, R. Miner, and W. Windsteiger, Eds., no. 07-06 in RISC-Linz Report Series, University of Linz, Austria, pp. 77-91. [ bib | .pdf ]

Dealing with a formal mathematical text (which we regard as a structured collection of hypotheses and conclusions), we often want to perform various analysis and transformation tasks on the initial formulas, without preliminary normalization. One particular example is checking for “ontological correctness”, namely, that every occurrence of a non-logical symbol stems from some definition of that symbol in the foregoing text. Generally, we wish to test whether some known fact (axiom, definition, lemma) is “applicable” at a given position inside a statement, and to actually apply it (when needed) in a logically sound way.

In this paper, we introduce the notion of a locally valid statement, a statement that can be considered true at a given position inside a first-order formula. We justify the reasoning about “innards” of a formula; in particular, we show that a locally valid equivalence is a sufficient condition for an equivalent transformation of a subformula. Using the notion of local validity, we give a formal definition of ontological correctness for a text written in a special formal language called ForTheL.

[9]

Verchinine, K., Lyaletski, A., and Paskevich, A. System for Automated Deduction (SAD): a tool for proof verification. In Automated Deduction, 21st International Conference, CADE-21 (Bremen, Germany, July 2007), F. Pfenning, Ed., vol. 4603 of Lecture Notes in Computer Science, Springer, pp. 398-403. [ bib | .pdf ]

In this paper, a proof assistant, called SAD, is presented. SAD deals with mathematical texts that are formalized in the ForTheL language (brief description of which is also given) and checks their correctness. We give a short description of SAD and a series of examples that show what can be done with it. Note that abstract notion of correctness on which the implementation is based, can be formalized with the help of a calculus (not presented here).

[10]

Paskevich, A. Connection tableaux with lazy paramodulation. In Automated Reasoning, 3rd International Joint Conference, IJCAR 2006 (Seattle WA, USA, Aug. 2006), U. Furbach and N. Shankar, Eds., vol. 4130 of Lecture Notes in Computer Science, Springer, pp. 112-124. [ bib | .pdf ]

It is well-known that the connection refinement of clause tableaux with paramodulation is incomplete (even with weak connections). In this paper, we present a new connection tableau calculus for logic with equality. This calculus is based on a lazy form of paramodulation where parts of the unification step become auxiliary subgoals in a tableau and may be subjected to subsequent paramodulations. Our calculus uses ordering constraints and a certain form of the basicness restriction.

[11]

Lyaletski, A., Paskevich, A., and Verchinine, K. SAD as a mathematical assistant - how should we go from here to there? Journal of Applied Logic 4, 4 (2006), 560-591. [ bib | .ps.gz ]

The System for Automated Deduction (SAD) is developed in the framework of the Evidence Algorithm research project and is intended for automated processing of mathematical texts. The SAD system works on three levels of reasoning: (a) the level of text presentation where proofs are written in a formal natural-like language for subsequent verification; (b) the level of foreground reasoning where a particular theorem proving problem is simplified and decomposed; (c) the level of background deduction where exhaustive combinatorial inference search in classical first-order logic is applied to prove end subgoals. We present an overview of SAD describing the ideas behind the project, the system's design, and the process of problem formalization in the fashion of SAD. We show that the choice of classical first-order logic as the background logic of SAD is not too restrictive. For example, we can handle binders like Σ or lim without resort to second order or to a full-powered set theory. We illustrate our approach with a series of examples, in particular, with the classical problem sqrt(2) not inQ.

[12]

Paskevych, A. Methods of formalization of mathematical knowledge and reasoning: theoretical and practical aspects. PhD thesis, Kiev National Taras Shevchenko University, 2005. In Ukrainian. [ bib | .pdf ]

[13]

Lyaletski, A., Verchinine, K., and Paskevich, A. Theorem proving and proof verification in the system SAD. In Mathematical Knowledge Management, 3rd International Conference, MKM 2004 (Bialowieza, Poland, Sept. 2004), A. Asperti, G. Bancerek, and A. Trybulec, Eds., vol. 3119 of Lecture Notes in Computer Science, Springer, pp. 236-250. [ bib | .ps.gz ]

In this paper, the current state of the System for Automated Deduction, SAD, is described briefly. The system may be considered as the modern vision of the Evidence Algorithm programme advanced by Academician V. Glushkov in early 1970s. V. Glushkov proposed to make investigation simultaneously into formalized languages for presenting mathematical texts in the form most appropriate for a user, formalization and evolutionary development of computer-made proof step, information environment having an influence on the evidence of a proof step, and man-assisted search for a proof. In this connection, SAD supports a number of formal languages for representing and processing mathematical knowledge along with the formal language ForTheL as their top representative, uses a sequent formalism developed for constructing an efficient technique of proof search within the signature of an initial theory, and gives a new way to organize the information environment for sharing mathematical knowledge among various computer services. The system SAD can be used to solve large variety of theorem proving problems including: establishing of the deducibility of sequents in first-order classical logic, theorem proving in ForTheL-environment, verifying correctness of self-contained ForTheL-texts, solving problems taken from the online library TPTP. A number of examples is given for illustrating the mathematical knowledge processing implemented in SAD.

[14]

Lyaletski, A. V., Doroshenko, A. E., Paskevich, A., and Verchinine, K. Evidential paradigm and intelligent mathematical text processing. In Information Systems Technology and its Applications, 3rd International Conference, ISTA 2004 (Salt Lake City UT, USA, July 2004), A. E. Doroshenko, T. A. Halpin, S. W. Liddle, and H. C. Mayr, Eds., vol. 48 of Lecture Notes in Informatics, GI, pp. 205-211. [ bib | .pdf ]

This paper presents the evidential paradigm of computer-supported mathematical assistance in “doing” mathematics and in reasoning activity. At present, the evidential paradigm is implemented in the form of System for Automated Deduction (SAD). The system is based on the methods of automated theorem proving and is intended for intelligent mathematical text processing. It proves mathematical theorems, verifies validity of self-contained mathematical texts and can be used for inference search in first-order sequent-based logic as well. For human-like representation of mathematical knowledge, SAD exploits an original formal language close to natural languages of scientific publications. Since the problem of automated text verification is of great importance for industrial applications (checking specifications, proving safety properties of network protocols, etc), the paper illustrates some principles and peculiarities of the evidential paradigm by means of exemplifying the verification of a part of a non-trivial mathematical text.

[15]

Lyaletski, A., Verchinine, K., and Paskevich, A. On verification tools implemented in the System for Automated Deduction. In Implementation Technology for Computational Logic Systems, 2nd CoLogNet Workshop, ITCLS 2003 (Pisa, Italy, Sept. 2003), pp. 3-14. [ bib | .ps.gz ]

Among the tasks of the Evidence Algorithm programme, the verification of formalized mathematical texts is of great significance. Our investigations in this domain were brought to practice in the last version of the System for Automated Deduction (SAD). The system exploits a formal language to represent mathematical knowledge in a “natural” form and a sequential first-order formalism to prove statements in the frame of a self-contained mathematical text. In the paper, we give an overview of the architecture of SAD and its verification tools. In order to demonstrate the work of SAD, a sample verification session is examined.

[16]

Verchinine, K., Lyaletski, A., and Paskevich, A. Applying the System for Automated Deduction to mathematical text verification. International Journal “Iskustvennyj Intellekt” 3 (2003), 57-69. In Russian. [ bib | .pdf ]

The paper is devoted to an approach to mathematical text processing in the style of Evidence Algorithm programme and describes the verification procedure implemented in the System for Automated Deduction (SAD). The Evidence Algorithm programme are aimed at construction of software systems for computer-aided mathematical activity, in particular, for automated theorem proving. The system SAD extracts and accumulates formalized mathematical knowledge and uses it to prove statements in the frame of a self-contained mathematical text. By now, the system SAD exploits a formal language for presenting mathematical texts and a sequent formalism that defines a notion of computer-made proof step. A mathematical text written is that language is translated into a structured sequence of first-order formulas which is verified then by means of a complete and sound sequent calculus. This verification scheme of SAD is explained by an example text from formal arithmetic.

[17]

Aselderov, Z., Verchinine, K., Lyaletski, A., Paskevich, A., Klimenko, V., and Fishman, Yu. Deductive, inductive, and analytic methods of presentation and processing of computer knowledge in the intellectual systems (1. Deductive methods and tools). “Matematychni mashyny i systemy” (3,4) (2003), 51-74. In Ukrainian. [ bib ]

[18]

Paskevich, A. A notion of local truth and its applications in automated theorem proving. Bulletin of the University of Kiev (physics and mathematics series) 1 (2003), 199-203. In Ukrainian. [ bib | .ps.gz ]

We investigate when a given statement can be considered true in a given position inside a formula. We show that we can consistently reason about interiors of a formula and argue that proposed methods can facilitate processing of a formalized mathematical text.

[19]

Verchinine, K., Degtyarev, A., Morokhovets, M., Lyaletski, A., and Paskevich, A. Evidence Algorithm and processing of formalized mathematical texts. International Journal “Problemy upravleniya i informatiki” 5 (2002), 80-95. In Russian. [ bib ]

[20]

Aselderov, Z., Verchinine, K., Degtyarev, A., Lyaletski, A., Paskevich, A., and Pavlov, A. Linguistic tools and deductive technique of the System for Automated Deduction. In Implementation of Logics, 3rd International Workshop, WIL 2002 (Tbilisi, Georgia, Oct. 2002), pp. 21-24. [ bib | .ps.gz ]

This paper is devoted to a brief description of some peculiarities and of the first software implementation of the System for Automated Deduction, SAD. Architecture of SAD corresponds well to a modern vision of the Evidence Algorithm that was conceived by V. Glushkov as a programme for constructing open systems for automated theorem proving that are intended for computer-aided “doing” mathematics: i.e. for extracting and accumulating mathematical computer knowledge and for using it in a regular and efficient manner to prove a given statement that is always considered as a part of a self-contained mathematical text. In addition, the main principles of SAD reflect the current understanding of the problem of man-assisted processing of mathematical computer knowledge.

[21]

Lyaletski, A., Verchinine, K., Degtyarev, A., and Paskevich, A. System for Automated Deduction (SAD): Linguistic and deductive peculiarities. In Intelligent Information Systems, 11th International Symposium, IIS 2002 (Sopot, Poland, June 2002), M. A. Klopotek, S. T. Wierzchon, and M. Michalewicz, Eds., Advances in Soft Computing, Physica-Verlag, pp. 413-422. [ bib | .ps.gz ]

In this paper a state-of-the-art of a system for automated deduction called SAD is described. An architecture of SAD corresponds well to a modern vision of the Evidence Algorithm programme initiated by Academician V. Glushkov. The system is intended for accumulating mathematical knowledge and using it in a regular and efficient manner for processing a self-contained mathematical text in order to prove a given statement that always is considered as a part of the text. Two peculiarities are inherent in SAD: (a) mathematical texts under consideration are formalized with the help of a specific formal language, which is close to a natural language used in mathematical publications; (b) proof search is based on a specific sequent-type calculus, which gives a possibility to formalize “natural reasoning style”. The language may be used as a tool to write and verify mathematical papers, theorems, and formal specifications, to perform model checking, and so on. The calculus is oriented to constructing some natural proof search methods such as definition and auxiliary proposition applications.

[22]

Aselderov, Z., Verchinine, K., Degtyarev, A., Lyaletski, A., and Paskevich, A. Peculiarities of mathematical text processing in the System for Automated Deduction (SAD). International Journal “Iskustvennyj Intellekt” 4 (2002), 163-171. In Russian. [ bib | .pdf ]

The goal of a research programme Evidence Algorithm is a development of an open system of automated proving that is able to accumulate mathematical knowledge and to prove theorems in a context of a self-contained mathematical text. By now, the first version of such a system called a System for Automated Deduction, SAD, is implemented in software. The system SAD possesses the following main features: mathematical texts are formalized using a specific formal language that is close to a natural language of mathematical publications; a proof search is based on special sequent-type calculi formalizing natural reasoning style, such as application of definitions and auxiliary propositions. These calculi also admit a separation of equality handling from deduction that gives an opportunity to integrate logical reasoning with symbolic calculation.

[23]

Lyaletski, A., and Paskevich, A. Goal-driven inference search in classical propositional logic. In Proc. International Workshop STRATEGIES'2001 (Siena, Italy, June 2001), pp. 65-74. [ bib | .ps.gz ]

Two goal-driven strategies for inference search in propositional logic are presented in the form of special sequent calculi. Some results on their soundness and completeness are given, and comparison of these calculi is made. It is shown that no one of them is preferable to another in the sense of constructing minimal inferences.

[24]

Lyaletski, A., and Paskevich, A. On some strategies of logical inference search that are driven by goals. Bulletin of the University of Kiev (physics and mathematics series) 2 (2001), 277-285. In Ukrainian. [ bib | .ps.gz ]

Two strategies for inference search in propositional logic are presented in the form of special sequential calculi. Some results on their soundness and completeness are given, and comparison of the calculi is made. It is shown that no one of them can be preferred to another in the sense of constructing minimal inferences.

[25]

Vershinin, K., and Paskevich, A. ForTheL - the language of formal theories. International Journal of Information Theories and Applications 7, 3 (2000), 120-126. [ bib | .ps.gz ]

The paper describes the language ForTheL (FORmal THEory Language) aimed at representation of formal theories - in strict mathematical sense of the term. Its syntax is strictly formalised in the terms of BNF and its semantics can be precisely defined with the help of syntactical transformation that maps ForTheL-phrases to the formulae of first-order logic with equality. At the same time ForTheL is intended to be close to the natural language of mathematical texts, it formalises and uses expressive means of the human language.

[26]

Paskevich, A. Peculiarities of the implementation of a high-level language for processing of mathematical texts. Bulletin of the University of Kiev (physics and mathematics series) 2 (1999), 284-288. In Ukrainian. [ bib | .ps.gz ]

New practical implementation of TL language and its features in comparison with the version used in SAD are considered. Description of the English TL version that was software implemented for the first time is given also.