Contradiction separation based dynamic multi-clause synergized automated deduction

قطعنامه به عنوان قواعد مشهور استنباط نقش کلیدی در استدلال خودکار بیش از پنج دهه ایفا کرده است. تعدادی از انواع و اصلاحیه های قطعنامه نیز مورد مطالعه قرار گرفته است، اساسا، همه آنها بر اساس قطعنامه باینری، یعنی قانون برش جفت مکمل است، در حالی که هر کسر شامل دو جمله می شود. در این مقاله، گسترش یک قانون قطعنامه باینری را پیشنهاد می کنیم که به عنوان یک قاعده اساسی مبتنی بر جداسازی جدید بر اساس قضیه خودکار پیشنهاد شده است، هدف قرار دادن مفاد پویا و چندگانه (دو یا چند) در یک روش هماهنگ، در حالی که رزولوشن باینری مورد خاص خود. سپس این تئوری کج خلقی اتوماتیک چند گانه مبتنی بر جداسازی تضاد است که پس از آن ثابت شده است که صدا و کامل است. توسعه این فرمت جدید نه تنها به نظر ما مبنی بر نشان دادن این است که چنین قاعدهیی از استنتاج میتواند عمومی باشد، بلکه همچنین با آرزوی ما این است که قاعدهی نتیجهگیری میتواند مبنایی برای الگوریتمهای و سیستمهای کسر خودکار خودکار باشد.