Abstract | ||
---|---|---|
The ADC method of proof search in propositional natural deduction proposed in 2000 proceeds bottom up first by Analysing the sequent into sub-goals by applying all possible introduction rules, and then by checking whether each of these sub-goals can be established using only elimination rules (Direct Chaining). This looks simpler than the worst case complexity (PSPACE) of the derivability problem ... |
Year | DOI | Venue |
---|---|---|
2016 | 10.1093/logcom/ext032 | Journal of Logic and Computation |
Keywords | Field | DocType |
Natural deduction,intuitionistic logic,polynomial decidability | Discrete mathematics,Proof search,Natural deduction,Sequent calculus,Algorithm,Proof complexity,Propositional variable,Mathematics | Journal |
Volume | Issue | ISSN |
26 | 1 | 0955-792X |
Citations | PageRank | References |
1 | 0.35 | 1 |
Authors | ||
2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Grigori Mints | 1 | 235 | 72.76 |
Shane Steinert-Threlkeld | 2 | 7 | 6.07 |