Borkar, Vivek S and Chandru, Vijay and Mitter, Sanjoy K (2002) Mathematical Programming Embeddings of Logic. In: Journal of Automated Reasoning, 29 (1). pp. 91-106.
Restricted to Registered users only
Download (123Kb) | Request a copy
Can theorem proving in mathematical logic be addressed by classical mathematical techniques like the calculus of variations? The answer is surprisingly in the affirmative, and this approach has yielded rich dividends from the dual perspective of better understanding of the mathematical structure of deduction and in improving the efficiency of algorithms for deductive reasoning. Most of these results have been for the case of propositional and probabilistic logics. In the case of predicate logic, there have been successes in adapting mathematical programming schemes to realize new algorithms for theorem proving using partial instantiation techniques. A structural understanding of mathematical programming embeddings of predicate logic would require tools from topology because of the need to deal with infinite-dimensional embeddings. This paper describes the first steps in this direction. General compactness theorems are proved for the embeddings, and some specialized results are obtained in the case of Horn logic.
|Item Type:||Journal Article|
|Additional Information:||Copyright of this article belongs to Springer.|
|Keywords:||Predicate logic;mathematical programming;CLP(R).|
|Department/Centre:||Division of Electrical Sciences > Computer Science & Automation (Formerly, School of Automation)|
|Date Deposited:||22 Jul 2008|
|Last Modified:||19 Sep 2010 04:47|
Actions (login required)