Name
Abstract | ||
|---|---|---|
We present a simple formulation of S. Maslov's inverse method of proof (and proof search) for first order predicate logic and illustrate it by proving decidability of validity for formulas with one existential quantifier and arbitrary function symbols. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-15025-8_26 | Fields of Logic and Computation |
Keywords | Field | DocType |
proof search,inverse method,arbitrary function symbol,existential quantifier,order predicate logic,class e,s. maslov,simple formulation,automated deduction,first order | Discrete mathematics,Proof search,Algebra,Existential quantification,Automated theorem proving,Inverse method,Decidability,First-order logic,Mathematics | Conference |
Volume | ISSN | ISBN |
6300 | 0302-9743 | 3-642-15024-1 |
Citations | PageRank | References |
3 | 0.45 | 3 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Grigori Mints | 1 | 235 | 72.76 |