{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:20:23Z","timestamp":1725488423471},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425250"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/3-540-44755-5_21","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T10:03:32Z","timestamp":1186740212000},"page":"297-312","source":"Crossref","is-referenced-by-count":1,"title":["A Certified Polynomial-Based Decision Procedure for Propositional Logic"],"prefix":"10.1007","author":[{"given":"Inmaculada","family":"Medina-Bulo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"1Francisco","family":"Palomo-Lozano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9 A.","family":"Alonso-Jim\u00e9nez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Aitken, W. E., Constable, R. L., Underwood, J. L.: Metalogical Frameworks II: Developing a Reflected Decision Procedure. J. Automated Reasoning 22(2) (1999)","DOI":"10.1023\/A:1005929703675"},{"key":"21_CR2","unstructured":"Boole, G. The Mathematical Analysis of Logic. Macmillan (1847)"},{"key":"21_CR3","unstructured":"Boyer, R. S., Moore, J S.: A Computational Logic. Academic Press (1978)"},{"key":"21_CR4","unstructured":"Boyer, R. S., Moore, J S.: Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures. In: Boyer, R. S., Moore, J S. (eds.): The Correctness Problem in Computer Science. Academic Press (1981)"},{"key":"21_CR5","unstructured":"Boyer, R. S., Moore, J S.: A Computational Logic Handbook. Academic Press. 2nd edn. (1998)"},{"key":"21_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055132","volume-title":"11th International Conference on Theorem Proving in Higher Order Logics","author":"J. L. Caldwell","year":"1998","unstructured":"Caldwell, J. L.: Classical Propositional Decidability via Nuprl Proof Extraction. 11th International Conference on Theorem Proving in Higher Order Logics. LNCS 1479 (1998)"},{"issue":"3","key":"21_CR7","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/S0747-7171(08)80043-0","volume":"11","author":"J. Chazarain","year":"1991","unstructured":"Chazarain, J., Riscos, A., Alonso, J. A., Briales, E.: Multi-Valued Logic and Gr\u00f6bner Bases with Applications to Modal Logic. J. Symbolic Computation 11 (1991)","journal-title":"Journal of Symbolic Computation"},{"key":"21_CR8","unstructured":"Harrison, J.: Metatheory and Reflection in Theorem Proving: A Survey and Critique. SRI International Cambridge Computer Science Research Centre. Technical Report CRC-053 (1995)"},{"issue":"2","key":"21_CR9","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1093\/comjnl\/38.2.162","volume":"38","author":"J. Harrison","year":"1995","unstructured":"Harrison, J.: Binary Decision Diagrams as a HOL Derived Rule. The Computer Journal 38 (1995)","journal-title":"The Computer Journal"},{"key":"21_CR10","series-title":"Lect Notes Comput Sci","volume-title":"9th International Conference on Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: Stlmarck\u2019s Algorithm as a HOL Derived Rule. 9th International Conference on Theorem Proving in Higher Order Logics. LNCS 1125 (1996)"},{"issue":"3","key":"21_CR11","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/0004-3702(85)90074-8","volume":"25","author":"Jieh Hsiang","year":"1985","unstructured":"Hsiang, J.: Refutational Theorem Proving using Term-Rewriting Systems. Artificial Intelligence 25 (1985)","journal-title":"Artificial Intelligence"},{"issue":"1-2","key":"21_CR12","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/S0747-7171(87)80024-X","volume":"3","author":"Jieh Hsiang","year":"1987","unstructured":"Hsiang, J.: Rewrite Method for Theorem Proving in First-Order Theory with Equality. J. Symbolic Computation 3 (1987)","journal-title":"Journal of Symbolic Computation"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Hsiang, J., Huang, G. S.: Some Fundamental Properties of Boolean Ring Normal Forms. DIMACS series on Discrete Mathematics and Computer Science: The Satisfiability Problem. AMS (1996)","DOI":"10.1090\/dimacs\/035\/16"},{"issue":"4","key":"21_CR14","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1109\/32.588534","volume":"23","author":"M. Kaufmann","year":"1997","unstructured":"Kaufmann, M., Moore, J S.: An Industrial Strength Theorem Prover for a Logic Based on Common Lisp. IEEE Trans, on Software Engineering 23(4) (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Moore, J S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers (2000)","DOI":"10.1007\/978-1-4757-3188-0"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Moore, J S.: Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers (2000)","DOI":"10.1007\/978-1-4757-3188-0"},{"issue":"4","key":"21_CR17","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1145\/1012497.1012521","volume":"10","author":"Deepak Kapur","year":"1985","unstructured":"Kapur, D., Narendran, P.: An Equational Approach to Theorem Proving in First-Order Predicate Calculus. 9th International Conference on Artificial Intelligence (1985)","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"issue":"1","key":"21_CR18","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/s005000050086","volume":"3","author":"L. M. Laita","year":"1999","unstructured":"Laita, L. M., Roanes-Lozano, E., Ledesma, L., Alonso, J. A.: A Computer Algebra Approach to Verification and Deduction in Many-Valued Knowledge Systems. Soft Computing 3(1) (1999)","journal-title":"Soft Computing"},{"key":"21_CR19","unstructured":"Medina-Bulo, I., Alonso-Jim\u00e9nez, J. A., Palomo-Lozano, F.: Automatic Verification of Polynomial Rings Fundamental Properties in ACL2. ACL2 Workshop 2000 Proceedings, Part A. The University of Texas at Austin, Department of Computer Sciences. Technical Report TR-00-29 (2000)"},{"key":"21_CR20","unstructured":"Medina-Bulo, I., Palomo-Lozano, F., Alonso-Jim\u00e9nez, J. A.: A Certified Algorithm for Translating Formulas into Polynomials. An ACL2 Approach. International Joint Conference on Automated Reasoning (2001)"},{"key":"21_CR21","unstructured":"Moore, J S.: Introduction to the OBDD Algorithm for the ATP Community. Computational Logic, Inc. Technical Report 84 (1992)"},{"issue":"5-6","key":"21_CR22","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1016\/S0747-7171(06)80007-6","volume":"15","author":"Christine Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C., Werner, B.: Synthesis of ML Programs in the System Coq. J. Symbolic Computation 15(5\u20136) (1993)","journal-title":"Journal of Symbolic Computation"},{"issue":"1","key":"21_CR23","first-page":"37","volume":"40","author":"M. H. Stone","year":"1936","unstructured":"Stone, M.: The Theory of Representation for Boolean Algebra. Trans. AMS 40 (1936)","journal-title":"Transactions of the American Mathematical Society"},{"key":"21_CR24","unstructured":"Sumners, R.: Correctness Proof of a BDD Manager in the Context of Satisfiability Checking. ACL2 Workshop 2000 Proceedings, Part A. The University of Texas at Austin, Department of Computer Sciences. Technical Report TR-00-29 (2000)"},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Th\u00e9ry, L. A Machine-Checked Implementation of Buchberger\u2019s Algorithm. J. Automated Reasoning 26 (2001)","DOI":"10.1023\/A:1026518331905"},{"key":"21_CR26","unstructured":"Wu, J., Tan, H.: An Algebraic Method to Decide the Deduction Problem in Prepositional Many-Valued Logics. International Symposium on Multiple-Valued Logics. IEEE Computer Society Press (1994)"},{"key":"21_CR27","unstructured":"Wu, J.: First-Order Polynomial Based Theorem Proving. In: Gao, X., Wang, D. (eds.): Mathematics Mechanization and Applications. Academic Press (1999)"},{"key":"21_CR28","unstructured":"Zhang, H.: A New Strategy for the Boolean Ring Based Approach to First Order Theorem Proving. Department of Computer Science. University of Iowa. Technical Report (1991)"},{"key":"21_CR29","unstructured":"Zhegalkin, I. I.: On a Technique of Evaluation of Propositions in Symbolic Logic. Mat. Sb. 34 (1927)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44755-5_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:25:52Z","timestamp":1619573152000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44755-5_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540425250"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-44755-5_21","relation":{},"subject":[]}}