CSE - A Automated Theorem Prover Based on Standard Contradiction Separation Dynamic Deduction

CSE - A Automated Theorem Prover Based on Standard Contradiction Separation Dynamic Deduction | Research Square window.SnipcartSettings = { analytics: { enabled: false } }; (function() { var accessVector = localStorage.getItem('access_vector') || ''; window.dataLayer = window.dataLayer || []; if (accessVector) { window.dataLayer.push({ user: { profile: { profileInfo: { snid: accessVector } } } }); } })(); (function(w,d,s,l,i){w[l]=w[l]||[];w[l].push({'gtm.start':new Date().getTime(),event:'gtm.js'});var f=d.getElementsByTagName(s)[0],j=d.createElement(s),dl=l!='dataLayer'?'&l='+l:'';j.async=true;j.src='https://www.googletagmanager.com/gtm.js?id='+i+dl;f.parentNode.insertBefore(j,f);})(window,document,'script','dataLayer','GTM-K279D39R'); Browse Preprints In Review Journals COVID-19 Preprints AJE Video Bytes Research Tools Research Promotion AJE Professional Editing AJE Rubriq About Preprint Platform In Review Editorial Policies Our Team Advisory Board Help Center Sign In Submit a Preprint Cite Share Download PDF Research Article CSE - A Automated Theorem Prover Based on Standard Contradiction Separation Dynamic Deduction Feng Cao, Jiafan Wang, Yang Xu, Jun Liu, Jianbing Yi This is a preprint; it has not been peer reviewed by a journal. https://doi.org/ 10.21203/rs.3.rs-3955960/v1 This work is licensed under a CC BY 4.0 License Status: Posted Version 1 posted You are reading this latest preprint version Abstract Contradiction Separation Extension (CSE in short), an automated theorem prover for first-order logic without equality, which is based on a novel standard contradiction separation (S-CS) inference rule. Different from binary resolution or its refinements, the biggest difference and characteristic of S-CS rule is that each resolution step can handle multiple (two or more) clauses for synergized deduction. This paper mainly describes problem format conversion, clause set preprocessing, deduction framework, distinctive heuristic strategies, S-CS dynamic inference mechanism in CSE. CSE is evaluated through benchmarks and the deduction characteristics of this multi-clause dynamic deduction are demonstrated, e.g., FOF division problems of CASC-26, CASC-J9. In addition, the CASC-J9 is also tested by combined systems, which combine CSE and other prover (Prover9, Eprover, Vampire), and the combined systems is applied to test on the hard problems with rating of 1. Experimental results show the CSE shows a competitive performance and can play a role in first-order logic automated theorem proving. automated theorem prover first-order logic contradiction separation inference heuristic strategies inference mechanism Full Text Cite Share Download PDF Status: Posted Version 1 posted You are reading this latest preprint version Research Square lets you share your work early, gain feedback from the community, and start making changes to your manuscript prior to peer review in a journal. As a division of Research Square Company, we’re committed to making research communication faster, fairer, and more useful. We do this by developing innovative software and high quality services for the global research community. Our growing team is made up of researchers and industry professionals working together to solve the most critical problems facing scientific publishing. Also discoverable on Platform About Our Team In Review Editorial Policies Advisory Board Help Center Resources Author Services Accessibility API Access RSS feed Manage Cookie Preferences © Research Square 2026 | ISSN 2693-5015 (online) Privacy Policy Terms of Service Do Not Sell My Personal Information {"props":{"pageProps":{"initialData":{"identity":"rs-3955960","acceptedTermsAndConditions":true,"allowDirectSubmit":true,"archivedVersions":[],"articleType":"Research Article","associatedPublications":[],"authors":[{"id":280987753,"identity":"d4f4d2eb-2242-430b-95b8-409d309725a4","order_by":0,"name":"Feng Cao","email":"","orcid":"","institution":"JiangXi University of Science and Technology","correspondingAuthor":false,"prefix":"","firstName":"Feng","middleName":"","lastName":"Cao","suffix":""},{"id":280987754,"identity":"72426e50-6fb5-46a0-a042-4c0ac829ab8a","order_by":1,"name":"Jiafan Wang","email":"","orcid":"","institution":"JiangXi University of Science and Technology","correspondingAuthor":false,"prefix":"","firstName":"Jiafan","middleName":"","lastName":"Wang","suffix":""},{"id":280987755,"identity":"f4f8fc3c-ed06-437e-bfbc-05b2d35b463d","order_by":2,"name":"Yang Xu","email":"","orcid":"","institution":"Southwest Jiaotong University","correspondingAuthor":false,"prefix":"","firstName":"Yang","middleName":"","lastName":"Xu","suffix":""},{"id":280987756,"identity":"b6a90893-5412-49ce-aff2-8eedcee7e274","order_by":3,"name":"Jun Liu","email":"data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAZAAAAAyAQMAAABI0h/eAAAABlBMVEX///8AAABVwtN+AAAACXBIWXMAAA7EAAAOxAGVKw4bAAAAwUlEQVRIie2RsQrCMBRFbyhkSnUWpP2FSEeh31IJ6C84dIgE6ubsUPQvnCOBTBU/wtWhIDiK6aRb4uaQs73HO3BvAkQifwiRidRYY/pZMa9CnNK5OxqqDBJI84uSSLIx6cGw/Khsj7oE77Q/mElPhnFLxR5WgF9kqEJZAVANfvU2GZTWBWvGD+AVrEjDYFni3kEHBFNEnlu7cl2WBRY7wSa++rOtMv29nme5Mjf0zzIbdZVHUd9TFfKRufciEolEIm80mj6lKZ0TZAAAAABJRU5ErkJggg==","orcid":"https://orcid.org/0000-0001-8859-5405","institution":"University of Ulster","correspondingAuthor":true,"prefix":"","firstName":"Jun","middleName":"","lastName":"Liu","suffix":""},{"id":280987757,"identity":"f4f169ba-0e14-444a-9489-01a9c486064a","order_by":4,"name":"Jianbing Yi","email":"","orcid":"","institution":"JiangXi University of Science and Technology","correspondingAuthor":false,"prefix":"","firstName":"Jianbing","middleName":"","lastName":"Yi","suffix":""}],"badges":[],"createdAt":"2024-02-14 11:39:47","currentVersionCode":1,"declarations":"","doi":"10.21203/rs.3.rs-3955960/v1","doiUrl":"https://doi.org/10.21203/rs.3.rs-3955960/v1","draftVersion":[],"editorialEvents":[],"editorialNote":"","failedWorkflow":false,"files":[{"id":61167731,"identity":"abee5d52-16f0-409d-90a5-21fb940b6aa8","added_by":"auto","created_at":"2024-07-26 13:45:53","extension":"pdf","order_by":1,"title":"","display":"","copyAsset":false,"role":"manuscript-pdf","size":490031,"visible":true,"origin":"","legend":"","description":"","filename":"SoftComputing2024.pdf","url":"https://assets-eu.researchsquare.com/files/rs-3955960/v1_covered_f1300750-b0b3-4a31-9a8e-3d71191f8c39.pdf"}],"financialInterests":"","formattedTitle":"CSE - A Automated Theorem Prover Based on Standard Contradiction Separation Dynamic Deduction","fulltext":[],"fulltextSource":"","fullText":"","funders":[],"hasAdminPriorityOnWorkflow":false,"hasManuscriptDocX":false,"hasOptedInToPreprint":true,"hasPassedJournalQc":"","hasAnyPriority":false,"hideJournal":true,"highlight":"","institution":"","isAcceptedByJournal":false,"isAuthorSuppliedPdf":true,"isDeskRejected":"","isHiddenFromSearch":false,"isInQc":false,"isInWorkflow":true,"isPdf":true,"isPdfUpToDate":true,"isWithdrawnOrRetracted":false,"journal":{"display":true,"email":"[email protected]","identity":"researchsquare","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":true,"externalIdentity":"","sideBox":"","snPcode":"","submissionUrl":"/submission","title":"Research Square","twitterHandle":"researchsquare","acdcEnabled":true,"dfaEnabled":false,"editorialSystem":"","reportingPortfolio":"","inReviewEnabled":false,"inReviewRevisionsEnabled":true},"keywords":"automated theorem prover, first-order logic, contradiction separation inference, heuristic strategies, inference mechanism","lastPublishedDoi":"10.21203/rs.3.rs-3955960/v1","lastPublishedDoiUrl":"https://doi.org/10.21203/rs.3.rs-3955960/v1","license":{"name":"CC BY 4.0","url":"https://creativecommons.org/licenses/by/4.0/"},"manuscriptAbstract":"\u003cp\u003eContradiction Separation Extension (CSE in short), an automated theorem prover for first-order logic without equality, which is based on a novel standard contradiction separation (S-CS) inference rule. Different from binary resolution or its refinements, the biggest difference and characteristic of S-CS rule is that each resolution step can handle multiple (two or more) clauses for synergized deduction. This paper mainly describes problem format conversion, clause set preprocessing, deduction framework, distinctive heuristic strategies, S-CS dynamic inference mechanism in CSE. CSE is evaluated through benchmarks and the deduction characteristics of this multi-clause dynamic deduction are demonstrated, e.g., FOF division problems of CASC-26, CASC-J9. In addition, the CASC-J9 is also tested by combined systems, which combine CSE and other prover (Prover9, Eprover, Vampire), and the combined systems is applied to test on the hard problems with rating of 1. Experimental results show the CSE shows a competitive performance and can play a role in first-order logic automated theorem proving.\u003c/p\u003e","manuscriptTitle":"CSE - A Automated Theorem Prover Based on Standard Contradiction Separation Dynamic Deduction","msid":"","msnumber":"","nonDraftVersions":[{"code":1,"date":"2024-03-21 08:20:06","doi":"10.21203/rs.3.rs-3955960/v1","editorialEvents":[{"type":"communityComments","content":0}],"status":"published","journal":{"display":true,"email":"[email protected]","identity":"researchsquare","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":true,"externalIdentity":"","sideBox":"","snPcode":"","submissionUrl":"/submission","title":"Research Square","twitterHandle":"researchsquare","acdcEnabled":true,"dfaEnabled":false,"editorialSystem":"","reportingPortfolio":"","inReviewEnabled":false,"inReviewRevisionsEnabled":true}}],"origin":"","ownerIdentity":"890d9deb-5c3f-429b-820d-66b996e94be4","owner":[],"postedDate":"March 21st, 2024","published":true,"recentEditorialEvents":[],"rejectedJournal":[],"revision":"","amendment":"","status":"posted","subjectAreas":[],"tags":[],"updatedAt":"2024-07-26T13:37:45+00:00","versionOfRecord":[],"versionCreatedAt":"2024-03-21 08:20:06","video":"","vorDoi":"","vorDoiUrl":"","workflowStages":[]},"version":"v1","identity":"rs-3955960","journalConfig":"researchsquare"},"__N_SSP":true},"page":"/article/[identity]/[[...version]]","query":{"redirect":"/article/rs-3955960","identity":"rs-3955960","version":["v1"]},"buildId":"qtupq5eGEP_6zYnWcrvyt","isFallback":false,"isExperimentalCompile":false,"dynamicIds":[84888],"gssp":true,"scriptLoader":[]}