A state vector algebra for algorithmic implementation of second-order logic
We present a mathematical framework for mapping second-order logic relations onto a simple state vector algebra. Using this algebra, basic theorems of set theory can be proven in an algorithmic way, hence by an expert system. We illustrate the use of the algebra with simple examples and show that, in principle, all theorems of basic set theory can be recovered in an elementary way. The developed technique can be used for an automated theorem proving in the 1st and 2nd order logic.
Code (0)
등록된 구현이 없습니다.
Tasks
Automated Theorem ProvingSimilar Papers 제목 키워드 기반
Kernel methods through the roof: handling billions of points efficiently
Kernel methods provide an elegant and principled approach to nonparametric learning, but so far could hardly be used in large scale problems, since na\"ive implementations scale poorly with data size. Recent advances hav…
GPUGaussian Process Regression for Inverse Problems in Linear PDEs
This paper introduces a computationally efficient algorithm in system theory for solving inverse problems governed by linear partial differential equations (PDEs). We model solutions of linear PDEs using Gaussian process…
Computational EfficiencyGaussian ProcessesregressionDifferentiable Parameter Optimization for DAEs with State-Dependent Events
Differential-algebraic equations (DAEs) with state-dependent events arise in systems whose continuous dynamics are constrained by algebraic equations and interrupted by mode changes, switching logic, impacts, or state re…
Clifford Group Equivariant Neural Networks
We introduce Clifford Group Equivariant Neural Networks: a novel approach for constructing $\mathrm{O}(n)$- and $\mathrm{E}(n)$-equivariant models. We identify and study the $\textit{Clifford group}$, a subgroup inside t…
Generic identification of binary-valued hidden Markov processes
The generic identification problem is to decide whether a stochastic process $(X_t)$ is a hidden Markov process and if yes to infer its parameters for all but a subset of parametrizations that form a lower-dimensional su…