1
vote
1answer
57 views

What paradigm of automated theorem proving is appropriate for Principia Mathematica-style formalization?

I am in possession of a book, which, inspired by Russell's Principia Mathematica (PM) and logical positivism, attempts to formalize a specific domain by determining axioms and deducing theorems from ...
0
votes
1answer
55 views

Some questions about strict tableau in propositional calculus (raising from a book by Melvin Fitting)

Recently, I encountered some questions when reading First-Order Logic and Automated Theorem Proving (1st ed - 1990), by Melvin Fitting. 1: confusing definition of strict tableau (page 39 definition ...
1
vote
2answers
135 views

Automatic theorem prover for proving simple theorems?

Is there a simple software that I could use to practice proving theorems in my course of mathematical logic? Basically what I need is ability to 1) define what axioms and laws I am allowed to use in ...
3
votes
1answer
87 views

What does Equational Theorem Prover do?

http://www.cs.unm.edu/~mccune/eqp/ What does EQP do? Is there any paper that explains what it does? README and other read files do not provide such information - it only talks of how to use it and ...
1
vote
1answer
66 views

Knuth-Bendix ordering and the one unary function

I'm looking at Knuth-Bendix ordering in the context of theorem proving with the superposition calculus. The explanations of KBO that I've been able to find say among other things that each function ...
14
votes
6answers
690 views

What are the theorems of mathematics proved by a computer so far?

By theorems, I mean the ones you can find in an undergraduate course of mathematics, not the ones you can find in a textbook of automated proofs. I mean by "proved by a computer" that an existing ...
2
votes
0answers
82 views

Ordering of multisets in “Paramodulation based theorem proving”

I'm reading this paper: http://www.lsi.upc.edu/~albert/papers/handbook.ps.gz and I can't understand a part of it. it defines an ordering on multisets (it defines a multiset over $A$ as a function $A ...
5
votes
4answers
426 views

How to start with automated theorem proving?

I'm interested in this question, but I'm not going to list my knowledge/demands but rather gear it to more general purpose; so the first thing concerns the prerequisites, i.e. How much ...
1
vote
1answer
86 views

Algorithm for enumerating theorems of first-order theories besides resolution

Is there a general algorithm for enumerating the theorems of any finite first-order theory with a better time complexity than simply using resolution on all first-order logic formulas?
2
votes
1answer
175 views

Superposition calculus and equality factoring

Superposition with equality resolution and equality factoring is said to be a complete calculus for first-order logic. The purpose of equality factoring is basically to get rid of paraduplicate ...