← Publications (BibTeX)
@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.
}
}
@article{LPV03II,
author = {Konstantin Verchinine and Alexander Lyaletski
and Andrey Paskevich},
title = {Applying the {System} for {Automated} {Deduction}
to mathematical text verification},
journal = {International Journal ``Iskustvennyj Intellekt''},
year = 2003,
volume = 3,
pages = {57--69},
note = {In Russian},
index = {986},
pdf = {papers/ii-03.ru.pdf},
abstract = {
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.
}
}
@article{AFKLPV03MMS,
author = {Z. Aselderov and K. Verchinine and A. Lyaletski and
A. Paskevich and V. Klimenko and {\mbox{Yu}}. Fishman},
title = {Deductive, inductive, and analytic methods of presentation
and processing of computer knowledge in the intellectual
systems (1. {Deductive} methods and tools)},
journal = {``Matematychni mashyny i systemy''},
year = 2003,
volume = {\mbox{(3,4)}},
pages = {51--74},
note = {In Ukrainian},
index = {987}
}
@article{P03VKU,
author = {Andrey Paskevich},
title = {A notion of local truth and its applications
in automated theorem proving},
journal = {Bulletin of the University of Kiev
(physics and mathematics series)},
year = 2003,
volume = 1,
pages = {199--203},
note = {In Ukrainian},
index = {988},
ps = {papers/vku-03.ua.ps.gz},
abstract = {
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.
}
}
@article{DLMPV02PUI,
author = {Konstantin Verchinine and Anatoli Degtyarev
and Marina Morokhovets and Alexander Lyaletski
and Andrey Paskevich},
title = {{Evidence} {Algorithm} and processing of formalized
mathematical texts},
journal = {International Journal ``Problemy upravleniya i informatiki''},
year = 2002,
volume = 5,
pages = {80--95},
note = {In Russian},
index = {989}
}
@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.
}
}
@article{ADLPV02II,
author = {Zainutdin Aselderov and Konstantin Verchinine
and Anatoli Degtyarev and Alexander Lyaletski
and Andrey Paskevich},
title = {Peculiarities of mathematical text processing in
the {System} for {Automated} {Deduction} ({SAD})},
journal = {International Journal ``Iskustvennyj Intellekt''},
year = 2002,
volume = 4,
pages = {163--171},
note = {In Russian},
index = {994},
pdf = {papers/ii-02.ru.pdf},
abstract = {
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.
}
}
@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{LP01VKU,
author = {Alexander Lyaletski and Andrey Paskevich},
title = {On some strategies of logical inference search
that are driven by goals},
journal = {Bulletin of the University of Kiev
(physics and mathematics series)},
year = 2001,
volume = 2,
pages = {277--285},
note = {In Ukrainian},
index = {996},
ps = {papers/vku-01.ua.ps.gz},
abstract = {
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.
}
}
@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.
}
}
@article{P99VKU,
author = {Andrey Paskevich},
title = {Peculiarities of the implementation of a high-level
language for processing of mathematical texts},
journal = {Bulletin of the University of Kiev
(physics and mathematics series)},
year = 1999,
volume = 2,
pages = {284--288},
note = {In Ukrainian},
index = {999},
ps = {papers/vku-99.ua.ps.gz},
abstract = {
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.
}
}
|