@article{DCKP16JAR,
author = {Dross, Claire and Conchon, Sylvain and Kanig, Johannes and Paskevich, Andrei},
title = {Adding Decision Procedures to {SMT} Solvers using Axioms with Triggers},
journal = {Journal of Automated Reasoning},
publisher = {Springer},
year = 2016,
volume = 56,
number = 4,
pages = {387--457},
index = {956},
pdf = {papers/jar-16.pdf},
abstract = {
SMT solvers are efficient tools to decide the
satisfiability of ground formulas, including a
number of built-in theories such as congruence,
linear arithmetic, arrays, and bit-vectors. Adding
theory to that list requires delving into the
implementation details of a given SMT solver, and
done mainly by the developers of the solver
itself. For many useful theories, one can
alternatively provide a first-order
axiomatization. However, in the presence of
quantifiers, SMT solvers are incomplete and exhibi
unpredictable behavior. Consequently, this approac
can not provide us with a complete and terminating
treatment of the theory of interest. In this paper
we propose a framework to solve this problem, base
on the notion of instantiation patterns, also know
as triggers. Triggers are annotations that suggest
instances which are more likely to be useful in
proof search. They are implemented in all SMT
solvers that handle first-order logic and are
included in the SMT-LIB format. In our framework,
the user provides a theory axiomatization with
triggers, along with a proof of completeness and
termination properties of this axiomatization, and
obtains a sound, complete, and terminating solver
for her theory in return. We describe and prove a
corresponding extension of the traditional Abstrac
DPLL Modulo Theory framework. Implementing this
mechanism in a given SMT solver requires a one-tim
development effort. We believe that this effort is
not greater than that of adding a single decision
procedure to the same SMT solver. We have
implemented the proposed extension in the Alt-Ergo
prover and we discuss some implementation details
the paper. To show that our framework can handle
complex theories, we prove completeness and
termination of a feature-rich axiomatization of
doubly-linked lists. Our tests show that our
approach results in a better performance of the
solver on goals that stem from the verification of
programs manipulating doubly-linked lists.}
}
@inproceedings{cfp15vstte,
author = {Martin Clochard and Jean-Christophe Filliâtre and Andrei Paskevich},
title = {How to avoid proving the absence of integer overflows},
editor = {Arie Gurfinkel and Sanjit A. Seshia},
booktitle = {VSTTE 2015, 7th Working Conference on Verified Software: Theories, Tools and Experiments},
month = jul,
year = 2015,
index = {957},
pdf = {papers/vstte-15.pdf},
abstract = {
When proving safety of programs, we must show, in particular,
the absence of integer overflows. Unfortunately, there are lots
of situations where performing such a proof is extremely difficult,
because the appropriate restrictions on function arguments are
invasive and may be hard to infer. Yet, in certain cases, we can
relax the desired property and only require the absence of overflow
during the first n steps of execution, n being large enough for all
practical purposes. It turns out that this relaxed property can be
easily ensured for large classes of algorithms, so that only a minimal
amount of proof is needed, if at all. The idea is to restrict the set
of allowed arithmetic operations on the integer values in question,
imposing a "speed limit" on their growth. For example, if we repeatedly
increment a 64-bit integer, starting from zero, then we will need at
least 2 to the power of 64 steps to reach an overflow; on current hardware,
this takes several hundred years. When we do not expect any single
execution of our program to run that long, we have effectively proved
its safety against overflows of all variables with controlled growth
speed. In this paper, we give a formal explanation of this approach,
prove its soundness, and show how it is implemented in the context
of deductive verification.}
}
@inproceedings{filliatre14cav,
author = {Jean-Christophe Filliâtre and Léon Gondelman and Andrei Paskevich},
title = {The Spirit of Ghost Code},
editor = {Armin Biere and Roderick Bloem},
booktitle = {CAV 2014, 26th International Conference on Computer Aided Verification},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {8559},
pages = {1-16},
month = jul,
year = 2014,
index = {958},
pdf = {papers/cav-14.pdf},
abstract = {
In the context of deductive program verification, ghost code is part
of the program that is added for the purpose of specification.
Ghost code must not interfere with regular code, in the sense that
it can be erased without any observable difference in the program outcome.
In particular, ghost data cannot participate in regular
computations and ghost code cannot mutate regular data or diverge.
The idea exists in the folklore since the early notion of auxiliary
variables and is implemented in many state-of-the-art program
verification tools. However, a rigorous definition and treatment of
ghost code is surprisingly subtle and few formalizations exist.
In this article, we describe a simple ML-style programming language
with mutable state and ghost code. Non-interference is ensured by a
type system with effects, which allows, notably, the same data types
and functions to be used in both regular and ghost code.
We define the procedure of ghost code erasure and we prove its
safety using bisimulation.
A similar type system, with numerous extensions which we briefly discuss,
is implemented in the program verification environment Why3.}
}
@inproceedings{cfmp14vstte,
author = {Martin Clochard and Jean-Christophe Filliâtre and Claude Marché and Andrei Paskevich},
title = {Formalizing Semantics with an Automatic Program Verifier},
booktitle = {VSTTE 2014, 6th International Conference on Verified Software: Theories, Tools, Experiments},
month = jul,
year = 2014,
editor = {Dimitra Giannakopoulou and Daniel Kroening},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
index = {959},
pdf = {papers/vstte-14.pdf},
abstract = {
A common belief is that formalizing semantics of programming
languages requires the use of a proof assistant providing
(1) a specification language with advanced features such as
higher-order logic, inductive definitions, type polymorphism,
and (2) a
corresponding proof environment where higher-order and inductive
reasoning can be performed, typically with user interaction.
In this paper we show that such a formalization is nowadays possible
inside a mostly-automatic program verification environment. We
substantiate this claim by formalizing several semantics for a
simple language, and proving their equivalence, inside the Why3
environment.}
}
@inproceedings{clochard14plpv,
author = {Martin Clochard and Claude Marché and Andrei Paskevich},
title = {Verified Programs with Binders},
booktitle = {PLPV 2014, ACM SIGPLAN Workshop on Programming Languages meets Program Verification},
year = 2014,
pages = {29-40},
publisher = {ACM Press},
index = {960},
pdf = {papers/plpv-14.pdf},
abstract = {
Programs that treat datatypes with binders, such as theorem provers or higher-order compilers, are regularly used for mission-critical purposes, and must be both reliable and performant. Formally proving such programs using as much automation as possible is highly desirable. In this paper, we propose a generic approach to handle datatypes with binders both in the program and its specification in a way that facilitates automated reasoning about such datatypes and also leads to a reasonably efficient code. Our method is implemented in the Why3 environment for program verification. We validate it on the examples of a lambda-interpreter with several reduction strategies and a simple tableaux-based theorem prover.}
}
@article{bobot14sttt,
author = {François Bobot and Jean-Christophe Filliâtre and Claude Marché and Andrei Paskevich},
title = {Let's Verify This with {Why3}},
journal = {International Journal on Software Tools for Technology Transfer},
url = {http://dx.doi.org/10.1007/s10009-014-0314-5},
year = 2014,
publisher = {Springer},
index = {961},
pdf = {papers/sttt-14.pdf},
abstract = {
We present solutions to the three challenges of the VerifyThis competition held at the 18th FM symposium in August 2012. These solutions use the Why3 environment for deductive program verification.}
}
@inproceedings{paskevich13cade,
author = {Jasmin C. Blanchette and Andrei Paskevich},
title = {{TFF1}: The {TPTP} typed first-order form with rank-1 polymorphism},
pages = {414-420},
booktitle = {CADE 2013, 24th International Conference on Automated Deduction},
month = jun,
year = 2013,
series = {Lecture Notes in Computer Science},
editor = {Maria Paola Bonacina},
volume = {7898},
publisher = {Springer},
index = {962},
pdf = {papers/cade-13.pdf},
abstract = {
The TPTP World is a well-established infrastructure for automatic theorem provers. It defines several concrete syntaxes, notably an untyped first-order form (FOF) and a typed first-order form (TFF0), that have become de facto standards. This paper introduces the TFF1 format, an extension of TFF0 with rank-1 polymorphism. The format is designed to be easy to process by existing reasoning tools that support ML-style polymorphism. It opens the door to useful middleware, such as monomorphizers and other translation tools that encode polymorphism in FOF or TFF0. Ultimately, the hope is that TFF1 will be implemented in popular automatic theorem provers.}
}
@inproceedings{bobot13vstte,
author = {François Bobot and Jean-Christophe Filliâtre and Claude Marché and Guillaume Melquiond and Andrei Paskevich},
title = {Preserving User Proofs Across Specification Changes},
pages = {191-201},
booktitle = {VSTTE 2013, 5th International Conference on Verified Software: Theories, Tools, Experiments},
month = may,
year = 2013,
editor = {Ernie Cohen and Andrey Rybalchenko},
series = {Lecture Notes in Computer Science},
volume = {8164},
publisher = {Springer},
index = {963},
pdf = {papers/vstte-13.pdf},
abstract = {
In the context of deductive program verification, both the specification and the code evolve as the verification process carries on. For instance, a loop invariant gets strengthened when additional properties are added to the specification. This causes all the related proof obligations to change; thus previous user verifications become invalid. Yet it is often the case that most of previous proof attempts (goal transformations, calls to interactive or automated provers) are still directly applicable or are easy to adjust. In this paper, we describe a technique to maintain a proof session against modification of verification conditions. This technique is implemented in the Why3 platform. It was successfully used in developing more than a hundred verified programs and in keeping them up to date along the evolution of Why3 and its standard library. It also helps out with changes in the environment, e.g. prover upgrades.}
}
@inproceedings{filliatre13esop,
author = {Jean-Christophe Filliâtre and Andrei Paskevich},
title = {{Why3} --- Where Programs Meet Provers},
booktitle = {ESOP 2013, Proceedings of the 22nd European Symposium on Programming},
month = mar,
year = {2013},
volume = {7792},
pages = {125-128},
series = {Lecture Notes in Computer Science},
editor = {Matthias Felleisen and Philippa Gardner},
publisher = {Springer},
index = {964},
pdf = {papers/esop-13.pdf},
abstract = {
We present Why3, a tool for deductive program verification, and WhyML,
its programming and specification language. WhyML is a first-order language with
polymorphic types, pattern matching, and inductive predicates. Programs can
make use of record types with mutable fields, type invariants, and ghost code.
Verification conditions are discharged by Why3 with the help of various existing
automated and interactive theorem provers. To keep verification conditions
tractable and comprehensible, WhyML imposes a static control of aliases that
obviates the use of a memory model. A user can write WhyML programs directly
and get correct-by-construction OCaml programs via an automated extraction
mechanism. WhyML is also used as an intermediate language for the verification
of C, Java, or Ada programs. We demonstrate the benefits of Why3 and WhyML on
non-trivial examples of program verification.
}
}
@inproceedings{dross12smt,
title = {Reasoning with Triggers},
author = {Dross, Claire and Conchon, Sylvain and Kanig, Johannes
and Paskevich, Andrei},
booktitle = {SMT 2012, 10th International Workshop on Satisability Modulo Theories},
editor = {Pascal Fontaine and Amit Goel},
address = {Manchester, UK},
month = jun,
year = {2012},
pages = {22-31},
index = {966},
pdf = {papers/smt-12.pdf},
abstract = {
SMT solvers can decide the satisfiability of ground formulas modulo a combination of
built-in theories. Adding a built-in theory to a given SMT solver is a complex and time
consuming task that requires internal knowledge of the solver. However, many theories
(arrays, reachability), can be easily expressed using first-order formulas.
Unfortunately, since universal quantifiers are not handled in a complete way by
SMT solvers, these axiomatics cannot be used as decision procedures.
In this paper, we show how to extend a generic SMT solver to accept a custom theory
description and behave as a decision procedure for that theory, provided that the described
theory is complete and terminating in a precise sense. The description language consists
of first-order axioms with triggers, an instantiation mechanism that is found in many SMT
solvers. This mechanism, which usually lacks a clear semantics in existing languages and
tools, is rigorously defined here; this definition can be used to prove completeness and
termination of the theory. We demonstrate using the theory of arrays, how such proofs
can be achieved in our formalism.
}
}
@techreport{dross12rr,
title = {Reasoning with Triggers},
author = {Dross, Claire and Conchon, Sylvain and Kanig, Johannes
and Paskevich, Andrei},
pages = {29},
type = {Research Report},
institution = {INRIA},
number = {RR-7986},
year = 2012,
month = jun,
index = {967},
pdf = {papers/rr7986-12.pdf},
url = {http://hal.inria.fr/hal-00703207},
abstract = {
SMT solvers can decide the satisfiability of ground
formulas modulo a combination of built-in
theories. Adding a built-in theory to a given SMT
solver is a complex and time consuming task that
requires internal knowledge of the solver. However,
many theories can be easily expressed using
first-order formulas. Unfortunately, since universal
quantifiers are not handled in a complete way by SMT
solvers, these axiomatics cannot be used as decision
procedures. In this paper, we show how to extend a
generic SMT solver to accept a custom theory
description and behave as a decision procedure for
that theory, provided that the described theory is
complete and terminating in a precise sense. The
description language consists of first-order axioms
with triggers, an instantiation mechanism that is
found in many SMT solvers. This mechanism, which
usually lacks a clear semantics in existing
languages and tools, is rigorously defined here;
this definition can be used to prove completeness
and termination of the theory. We demonstrate on two
examples, how such proofs can be achieved in our
formalism.}
}
@inproceedings{filliatre12compare,
author = {Jean-Christophe Filliâtre and Andrei Paskevich and Aaron Stump},
title = {The 2nd Verified Software Competition: Experience Report},
booktitle = {COMPARE2012, 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems},
address = {Manchester, UK},
month = jun,
year = 2012,
editor = {Vladimir Klebanov and Bernhard Beckert and Armin Biere and Geoff Sutcliffe},
series = {CEUR Workshop Proceedings},
volume = {873},
pages = {36--49},
index = {968},
pdf = {papers/compare-12.pdf},
abstract = {
We report on the second verified software competition. It was
organized by the three authors on a 48 hours period on November
8--10, 2011. This paper describes the competition, presents the
five problems that were proposed to the participants, and gives
an overview of the solutions sent by the 29 teams that entered
the competition.}
}
@inproceedings{BP2011frocos,
author = {François Bobot and Andrei Paskevich},
title = {Expressing Polymorphic Types in a Many-Sorted Language},
editor = {Tinelli, Cesare and Sofronie-Stokkermans, Viorica},
booktitle = {FroCoS 2011, 8th International Symposium on Frontiers of Combining Systems},
series = {Lecture Notes in Computer Science},
volume = {6989},
year = {2011},
pages = {87--102},
month = oct,
publisher = {Springer},
address = {Saarbrücken, Germany},
index = {969},
pdf = {papers/frocos-11.pdf},
abstract = {
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.
}
}
@misc{BP2011report,
author = {François Bobot and Andrei Paskevich},
title = {Expressing Polymorphic Types in a Many-Sorted Language},
note = {Extended report},
url = {http://hal.inria.fr/inria-00591414/en/},
month = jul,
year = 2011,
index = {970},
pdf = {papers/polyfol-11.pdf},
abstract = {
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.
}
}
@inproceedings{BFMP11boogie,
author = {François Bobot and Jean-Christophe Filliâtre and Claude Marché and Andrei Paskevich},
title = {{Why3}: Shepherd Your Herd of Provers},
booktitle = {Boogie 2011, First International Workshop on Intermediate Verification Languages},
year = 2011,
pages = {53--64},
address = {Wrocław, Poland},
month = aug,
index = {971},
pdf = {papers/boogie-11.pdf},
abstract = {
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.
}
}
@inproceedings{CCFPPU10PEPM,
author = {{\'E}velyne Contejean and Pierre Courtieu and Julien Forest
and Andrei Paskevich and Olivier Pons and Xavier Urbain},
title = {{A3PAT}, an approach for certified automated termination proofs},
booktitle = {PEPM'10, Proceedings of the 2010 ACM SIGPLAN Workshop on
Partial Evaluation and Program Manipulation},
publisher = {ACM},
address = {Madrid, Spain},
month = jan,
year = {2010},
pages = {63--72},
doi = {http://doi.acm.org/10.1145/1706356.1706370},
index = {972},
pdf = {papers/pepm-10.pdf},
abstract = {
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.
}
}
@inproceedings{VLPA08MKM,
author = {Konstantin Verchinine and Alexander Lyaletski
and Andrei Paskevich and Anatoly Anisimov},
title = {On correctness of mathematical texts from
a logical and practical point of view},
booktitle = {Intelligent Computer Mathematics, AISC/Calculemus/MKM 2008},
editor = {Serge Autexier and John Campbell and Julio Rubio
and Volker Sorge and Masakazu Suzuki and Freek Wiedijk},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
address = {Birmingham, United Kingdom},
month = jul,
year = 2008,
volume = 5144,
pages = {583--598},
index = {973},
pdf = {papers/mkm-08.pdf},
abstract = {
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.
}
}
@article{P08JAR,
author = {Andrei Paskevich},
title = {Connection Tableaux with Lazy Paramodulation},
journal = {Journal of Automated Reasoning},
publisher = {Springer},
year = 2008,
volume = 40,
number = {2--3},
pages = {179--194},
index = {974},
pdf = {papers/jar-08.pdf},
abstract = {
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.
}
}
@phdthesis{P07THES,
author = {Andriy Paskevych},
title = {Méthodes de formalisation des connaissances
et des raisonnements mathématiques:
aspects appliqués et théoriques},
school = {Université Paris 12},
year = 2007,
pages = {128},
note = {In French},
index = {975},
pdf = {papers/thesis-07.fr.pdf},
abstract = {
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.
}
}
@inproceedings{PVLA07MKM,
author = {Andrei Paskevich and Konstantin Verchinine
and Alexander Lyaletski and Anatoly Anisimov},
title = {Reasoning inside a formula and ontological correctness
of a formal mathematical text},
booktitle = {Calculemus/MKM 2007 --- Work in Progress},
editor = {Manuel Kauers and Manfred Kerber and Robert Miner
and Wolfgang Windsteiger},
series = {RISC-Linz Report Series, University of Linz, Austria},
address = {Hagenberg, Austria},
month = jun,
year = 2007,
number = {07-06},
pages = {77--91},
index = {976},
pdf = {papers/mkm-07.pdf},
abstract = {
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.
}
}
@inproceedings{VLP07CADE,
author = {Konstantin Verchinine and Alexander Lyaletski
and Andrei Paskevich},
title = {{System for Automated Deduction (SAD): a tool
for proof verification}},
booktitle = {Automated Deduction, 21st International Conference, CADE-21},
editor = {Frank Pfenning},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
address = {Bremen, Germany},
month = jul,
year = 2007,
volume = 4603,
pages = {398--403},
index = {977},
pdf = {papers/cade-07.pdf},
abstract = {
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).
}
}
@inproceedings{P06IJCAR,
author = {Andrei Paskevich},
title = {Connection Tableaux with Lazy Paramodulation},
booktitle = {Automated Reasoning, 3rd International
Joint Conference, IJCAR 2006},
editor = {Uli Furbach and Natarajan Shankar},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
address = {Seattle WA, USA},
month = aug,
year = 2006,
volume = 4130,
pages = {112--124},
index = {978},
pdf = {papers/ijcar-06.pdf},
abstract = {
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.
}
}
@article{LPV06JAL,
author = {Alexander Lyaletski and Andrey Paskevich
and Konstantin Verchinine},
title = {{SAD} as a mathematical assistant --- how
should we go from here to there?},
journal = {Journal of Applied Logic},
booktitle = {Towards Computer Aided Mathematics},
editor = {Christoph Benzm\"uller},
publisher = {Elsevier},
year = 2006,
volume = 4,
number = 4,
pages = {560--591},
index = {980},
ps = {papers/jal-06.ps.gz},
abstract = {
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 $\mathit{\Sigma}$
or $\mathit{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\in \mathbf{Q}$.
}
}
@phdthesis{P05THES,
author = {Andriy Paskevych},
title = {Methods of formalization of mathematical knowledge
and reasoning: theoretical and practical aspects},
school = {Kiev National Taras Shevchenko University},
year = 2005,
note = {In Ukrainian},
pages = {140},
index = {981},
pdf = {papers/thesis-05.ua.pdf}
}
@inproceedings{LPV04MKM,
author = {Alexander Lyaletski and Konstantin Verchinine
and Andrey Paskevich},
title = {Theorem Proving and Proof Verification in the System {SAD}},
booktitle = {Mathematical Knowledge Management,
3rd International Conference, MKM 2004},
editor = {Andrea Asperti and Grzegorz Bancerek and Andrzej Trybulec},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
address = {Bialowieza, Poland},
month = sep,
year = 2004,
volume = 3119,
pages = {236--250},
index = {982},
ps = {papers/mkm-04.ps.gz},
abstract = {
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.
}
}
@inproceedings{LDPV04ISTA,
author = {Alexander V. Lyaletski and Anatoly E. Doroshenko
and Andrey Paskevich and Konstantin Verchinine},
title = {Evidential Paradigm and Intelligent
Mathematical Text Processing},
booktitle = {Information Systems Technology and its Applications,
3rd International Conference, ISTA 2004},
editor = {Anatoly E. Doroshenko and Terry A. Halpin
and Stephen W. Liddle and Heinrich C. Mayr},
series = {Lecture Notes in Informatics},
publisher = {GI},
address = {Salt Lake City UT, USA},
month = jul,
year = 2004,
volume = 48,
pages = {205--211},
index = {983},
pdf = {papers/ista-04.pdf},
abstract = {
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.
}
}
@inproceedings{LPV03ITCLS,
author = {Alexander Lyaletski and Konstantin Verchinine
and Andrey Paskevich},
title = {On Verification Tools Implemented in the {System}
for {Automated} {Deduction}},
booktitle = {Implementation Technology for Computational
Logic Systems, 2nd CoLogNet Workshop, ITCLS 2003},
address = {Pisa, Italy},
month = sep,
year = 2003,
pages = {3--14},
index = {984},
ps = {papers/itcls-03.ps.gz},
abstract = {
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.
}
}
@inproceedings{ADLPPV02WIL,
author = {Zainutdin Aselderov and Konstantin Verchinine
and Anatoli Degtyarev and Alexander Lyaletski
and Andrey Paskevich and Alexandre Pavlov},
title = {Linguistic Tools and Deductive Technique of the
{System} for {Automated} {Deduction}},
booktitle = {Implementation of Logics, 3rd International
Workshop, WIL 2002},
address = {Tbilisi, Georgia},
month = oct,
year = 2002,
pages = {21--24},
index = {991},
ps = {papers/wil-02.ps.gz},
abstract = {
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.
}
}
@inproceedings{DLPV02IIS,
author = {Alexander Lyaletski and Konstantin Verchinine
and Anatoli Degtyarev and Andrey Paskevich},
title = {{System} for {Automated} {Deduction} ({SAD}):
Linguistic and Deductive Peculiarities},
booktitle = {Intelligent Information Systems, 11th International
Symposium, IIS 2002},
editor = {M. A. Klopotek and S. T. Wierzchon and M. Michalewicz},
series = {Advances in Soft Computing},
publisher = {Physica-Verlag},
address = {Sopot, Poland},
month = jun,
year = 2002,
pages = {413--422},
index = {992},
ps = {papers/iis-02.ps.gz},
abstract = {
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.
}
}
@inproceedings{LP01STRAT,
author = {Alexander Lyaletski and Andrey Paskevich},
title = {Goal-driven inference search in classical propositional logic},
booktitle = {Proc. International Workshop {STRATEGIES'2001}},
address = {Siena, Italy},
month = jun,
year = 2001,
pages = {65--74},
index = {995},
ps = {papers/strat-01.ps.gz},
abstract = {
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.
}
}
@article{PV00ITA,
author = {Konstantin Vershinin and Andrey Paskevich},
title = {{ForTheL} --- the language of formal theories},
journal = {International Journal of Information
Theories and Applications},
year = 2000,
volume = 7,
number = 3,
pages = {120--126},
index = {998},
ps = {papers/ita-00.ps.gz},
abstract = {
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.
}
}
Last update: 5 Sep 2015