In contrast to widely known sequential and resolution approaches to the automatic deduction of theorems, we propose a language and calculi that are based on a representation of predicate calculus with the help of standard quantifiers [\textit{N. Bourbaki}, Théorie des ensembles (1958; Zbl 0092.27901)] that are used in deduction of theorems of the method of comparison in mathematical systems theory [\textit{V. M. Matrosov}, \textit{L. Yu. Anapol'skij} and \textit{S. N. Vasil'ev}: Comparison method in mathematical systems theory (Russian) (1980; Zbl 0468.93002)]. In addition to a descriptive version of the calculus, we propose a constructive version in the spirit of \textit{A. N. Kolmogorov's} calculus of problems [Math. Z. 35, 58-65 (1932; Zbl 0004.00201)].
This page was built for publication: Calculus of standard quantor formulas
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1363870)
