Literal Chunk Contradiction and Clause Regular Contradiction in Propositional Logic
The resolution principle is a concise,reliable,and complete inference rule in automatic reasoning.The contradiction sepa-ration-based dynamic multi-clause synergized automated deduction is an extension of the resolution principle,and the contradiction is the theory's core part.Due to the complex structure of the contradiction and the few generation strategies,a new strategy for generating the contradiction is proposed,i.e.,multiple standard contradictions are used to generate the literal chunk contradic-tion.Then,a new contradiction is obtained by adding complementary contradiction sets.The focus is on the nature of the contra-diction generated by the literal chunk contradiction with a special structure,i.e.,the clause regular contradiction,which shows that the clause regular contradiction with a specific structure is still a contradiction after adding the clause.Finally,an algorithm for generating contradiction is proposed,which provides a reference for generating new contradictions on computers.
Standard contradictionPropositional logicLiteral chunk contradictionClause regular contradiction
NETL
NSTL
万方数据
