# Generating theorem proving procedures from axioms of Truncated Predicate Calculus

## TL;DR

This paper introduces a new method for automated theorem proving that generates polynomial cost procedures from axioms within Truncated Predicate Calculus, demonstrating promising results on example problems.

## Contribution

It presents a novel approach to automated theorem proving by generating efficient procedures based on axioms of Truncated Predicate Calculus, a subset of standard predicate calculus.

## Key findings

- Procedures recognize sentences in the theory with polynomial cost
- Approach demonstrated on several example problems
- Shows potential for efficient automated theorem proving

## Abstract

We present a~novel approach to the problem of automated theorem proving. Polynomial cost procedures that recognise sentences belonging to a theory are generated on a basis of a set of axioms of the so-called Truncated Predicate Calculus being a~subset of standard predicate calculus. Several exemplary problems are included to show the performance of the proposed approach.