Resolution for Constrained Pseudo-Propositional Logic
This work, shows how propositional resolution can be generalized to obtain a resolution proof system for constrained pseudo-propositional logic (CPPL), which is an extension resulted from inserting the natural numbers with few constraints symbols into the alphabet of propositional logic and adjusting the underling language accordingly. Unlike the construction of CNF formulas which are restricted to a finite set of clauses, the extended CPPL does not require the corresponding set to be finite. Although this restriction is made dispensable, this work presents a constructive proof showing that the generalized resolution for CPPL is sound and complete. As a marginal result, this implies that propositional resolution is also sound and complete for formulas with even infinite set of clauses.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
On Forgetting in Tractable Propositional Fragments
Distilling from a knowledge base only the part that is relevant to a subset of alphabet, which is recognized as forgetting, has attracted extensive interests in AI community. In standard propositional logic, a general al…
A First Polynomial Non-Clausal Class in Many-Valued Logic
The relevance of polynomial formula classes to deductive efficiency motivated their search, and currently, a great number of such classes is known. Nonetheless, they have been exclusively sought in the setting of clausal…
FormRepresentation Theorems for Cumulative Propositional Dependence Logics
This paper establishes and proves representation theorems for cumulative propositional dependence logic and for cumulative propositional logic with team semantics. Cumulative logics are famously given by System C. For pr…
Encoding Argumentation Frameworks to Propositional Logic Systems
The theory of argumentation frameworks ($AF$s) has been a useful tool for artificial intelligence. The research of the connection between $AF$s and logic is an important branch. This paper generalizes the encoding method…
Tableaux for Dynamic Logic of Propositional Assignments
The Dynamic Logic for Propositional Assignments (DL-PA) has recently been studied as an alternative to Propositional Dynamic Logic (PDL). In DL-PA, the abstract atomic programs of PDL are replaced by assignments of propo…