Evidence Algorithm and Sequent Logical Inference Search. - Anatoli Degtyarev; Alexander V. Lyaletski; Marina K. Morokhovets (LPAR, 1999)

On linguistic aspects of integration of computer mathematical knowledge. - Alexander V. Lyaletski; Marina Morokovets (Calculemus, 1999)

Quantifier Handling Issues in Computer-Oriented Intuitionistic Calculi. - Alexander V. Lyaletski (Intelligent Information Systems, 2001)

System for Automated Deduction (SAD): Linguistic and Deductive Peculiarities. - Alexander V. Lyaletski; Konstantin Verchinine; Anatoli Degtyarev; Andrey Paskevich (Intelligent Information Systems, 2002)

Computer-Oriented Sequent Inferring without Preliminary Skolemization. - Alexander V. Lyaletski (IIS, 2003)

On Admissible Substitutions in Classical and Intuitionistic Sequent Logics. - Alexander V. Lyaletski (Intelligent Information Systems, 2004)

Evidential Paradigm and Intelligent Mathematical Text Processing. - Alexander V. Lyaletski; Anatoly E. Doroshenko; Andrey Paskevich; Konstantin Verchinine (ISTA, 2004)

Theorem Proving and Proof Verification in the System SAD. - Alexander V. Lyaletski; Andrey Paskevich; Konstantin Verchinine (MKM, 2004)

Literal Trees and Resolution Technique. - Alexander V. Lyaletski; Alexander A. Letichevsky; Oleksandr Kalinovskyy (Intelligent Information Systems, 2005)

Tableau Method with Free Variables for Intuitionistic Logic. - Boris Konev; Alexander V. Lyaletski (Intelligent Information Systems, 2006)

On Herbrand's Theorem for Intuitionistic Logic. - Alexander V. Lyaletski; Boris Konev (JELIA, 2006)

The SAD System in Three Dimensions. - Anatoly V. Anisimov; Alexander V. Lyaletski (SYNASC, 2006)

Sequent forms of Herbrand theorem and their applications. - Alexander V. Lyaletski (Ann. Math. Artif. Intell., 2006)

SAD as a mathematical assistant - how should we go from here to there? - Alexander V. Lyaletski; Andrey Paskevich; Konstantin Verchinine (J. Appl. Log., 2006)

System for Automated Deduction (SAD): A Tool for Proof Verification. - Konstantin Verchinine; Alexander V. Lyaletski; Andrey Paskevich (CADE, 2007)

On Correctness of Mathematical Texts from a Logical and Practical Point of View. - Konstantin Verchinine; Alexander V. Lyaletski; Andrey Paskevich; Anatoly V. Anisimov (AISC/MKM/Calculemus, 2008)

On Some Problems of Efficient Inference Search in First-Order Cut-Free Modal Sequent Calculi. - Alexander V. Lyaletski (SYNASC, 2008)

On Herbrand-like Theorems for Cut-free Modal Sequent Logics. - Alexander V. Lyaletski (SYNASC, 2009)

Evidence Algorithm and System for Automated Deduction: A Retrospective View. - Alexander V. Lyaletski; Konstantin Verchinine (AISC/MKM/Calculemus, 2010)

Intelligent Testing in Kyiv: Analytical and Deductive Paradigms and their Implementation. - Vitaly Klimenko; Alexander V. Lyaletski (ICTERI, 2012)

C-Clause Calculi and Refutation Search in First-Order Classical Logic. - Alexander V. Lyaletski (ICTERI, 2015)

Admissibility, compatibility, and deducibility in first-order sequent logics. - Alexander V. Lyaletski (Comput. Sci. J. Moldova, 2015)

Evidence Algorithm and Inference Search in First-Order Logics. - Alexander V. Lyaletski (J. Autom. Reason., 2015)

Evidential Paradigm as Formal Knowledge Presentation and Processing. - Alexander V. Lyaletski; Alexandre Lyaletsky; Andrei Paskevich (ICTERI, 2016)

Mathematical Text Processing in EA-style: a Sequent Aspect. - Alexander V. Lyaletski (J. Formaliz. Reason., 2016)

The SAD System: a Current State and Future Work. - Alexander V. Lyaletski; Alexandre Lyaletsky; Konstantin Verchinine (ICTERI, 2017)

Evidence Algorithm Approach to Automated Theorem Proving and SAD Systems. - Alexander V. Lyaletski; Alexandre Lyaletsky (IT&I, 2020)

On One Approach to Goal-Driven Proof Search in Classical First-Order Logic. - Alexander V. Lyaletski; Alexandre Lyaletsky (SYNASC, 2020)