First-order logic as a constraint satisfaction problem
| Autor: | Robert M. Haralick, Hirohiko Kushida |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
Predicate logic
Soundness Computer science Craig interpolation 02 engineering and technology Propositional calculus Decidability First-order logic Algebra Constraint (information theory) TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Artificial Intelligence TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science 020204 information systems 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Constraint satisfaction problem |
| Zdroj: | Progress in Artificial Intelligence. 10:375-389 |
| ISSN: | 2192-6360 2192-6352 |
| DOI: | 10.1007/s13748-021-00240-8 |
| Popis: | In this paper, we discourse an analysis of classical first-order predicate logic as a constraint satisfaction problem, CSP. First, we will offer our general framework for CSPs, and then apply it to first-order logic. We claim it would function as a new semantics, constraint semantics, for logic. Then, we prove the soundness and completeness theorems with respect to the constraint semantics. The latter theorem, which will be proven by a proof-search method, implies the cut-elimination theorem. Furthermore, using the constraint semantics, we make a new proof of the Craig interpolation theorem. Also, we will provide feasible algorithms to generate interpolants for some decidable fragments of first-order logic: the propositional logic and the monadic fragments. The algorithms, reflecting a ‘projection’ of an indexed relation, will show how to transform given formulas syntactically to obtain interpolants. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink