Search results for "Theorem-proving"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
84	Quan Liu, Yang Gao 0001, Zhiming Cui, WangShu Yao, ZhongWen Chen	An Tableau Automated Theorem Proving Method Using Logical Reinforcement Learning.	ISICA	2007	DBLP DOI BibTeX RDF	logical reinforcement learning, tableau automated theorem proving, LOMDP
75	Sandip Ray, Rob Sumners	Combining Theorem Proving with Model Checking through Predicate Abstraction.	IEEE Des. Test Comput.	2007	DBLP DOI BibTeX RDF	model checking, formal verification, theorem proving, predicate abstraction, ACL2
75	Sun Yong-qiang, Lu Ru-zhan, Bi Hua	Program synthesis based on Boyer-Moore theorem proving techniques.	ACM Conference on Computer Science	1985	DBLP DOI BibTeX RDF	Boyer-Moore technique, program sysnthesis, theorem proving, resolution
71	Youngsik Kim, Parija Sule, Nazanin Mansouri	Exploiting PSL standard assertions in a theorem-proving-based verification environment.	ACM Great Lakes Symposium on VLSI	2005	DBLP DOI BibTeX RDF	assertion-based design, modeling, verification, theorem-proving, formal semantics, PSL
70	Maria Paola Bonacina, Jieh Hsiang	On Fairness of Completion-Based Theorem Proving Strategies.	RTA	1991	DBLP DOI BibTeX RDF
67	Sreeranga P. Rajan, Jeffrey J. Joyce, Carl-Johan H. Seger	From Abstract Data Types to Shift Registers: A Case Study in Formal Specification and Verification at Differing Levels of Abstraction using Theorem Proving and Symbolic Simulation.	HUG	1993	DBLP DOI BibTeX RDF
66	Wing-Kwong Wong, Bo-Yu Chan, Sheng-Kai Yin	A Dynamic Geometry Environment for Learning Theorem Proving.	ICALT	2005	DBLP DOI BibTeX RDF	learning geometry, geometry education, theorem proving, Dynamic geometry
66	Hongbo Li 0012	Algebraic Representation, Elimination and Expansion in Automated Geometric Theorem Proving.	Automated Deduction in Geometry	2002	DBLP DOI BibTeX RDF	Cayley algebra, bracket algebra, affine geometry, automated theorem proving, projective geometry, conics
66	Miroslav Popovic, Vladimir Kovacevic, Ivan Velikic	A Formal Software Verification Concept Based on Automated Theorem Proving and Reverse Engineering.	ECBS	2002	DBLP DOI BibTeX RDF	formal software verification, fault-tolerant and robust software, mission-critical embedded software, reverse engineering, automated theorem proving, predicate calculus
66	Fausto Giunchiglia, Paolo Traverso	Theorem proving in technology transfer: the user's point of view.	Int. J. Softw. Tools Technol. Transf.	2000	DBLP DOI BibTeX RDF	Formal methods, Mechanized theorem proving
65	Jieh Hsiang, Mandayam K. Srivas	PROLOG-Based Inductive Theorem Proving.	FSTTCS	1985	DBLP DOI BibTeX RDF
64	Mark D. Aagaard, Robert B. Jones, Carl-Johan H. Seger	Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving.	TPHOLs	1999	DBLP DOI BibTeX RDF
62	Larry Wos	Solving Open Questions with an Automated Theorem-Proving Program.	CADE	1982	DBLP DOI BibTeX RDF
62	Weiqiang Kong, Takahiro Seino, Kokichi Futatsugi, Kazuhiro Ogata 0001	A Lightweight Integration of Theorem Proving and Model Checking for System Verification.	APSEC	2005	DBLP DOI BibTeX RDF
61	Chih-Hung Wu, Shie-Jue Lee	On parallelism of hyper-linking theorem proving: a preliminary report.	ICPADS	1996	DBLP DOI BibTeX RDF	hyper-linking theorem proving, hyper-linking proof procedure, phase-level, clause-level, literal-level, search level parallelism, parallel strategies, parallel algorithms, parallelism, artificial intelligence, parallel architectures, theorem proving
61	Ming-Yi Fang, Wen-Tsuen Chen	Vectorization of a Generalized Procedure for Theorem Proving in Propositional Logic on Vector Computers.	IEEE Trans. Knowl. Data Eng.	1992	DBLP DOI BibTeX RDF	artificial intelligence, theorem proving, theorem proving, formal logic, propositional logic, vector processor systems, vectorisation, vector computers, deduction rules
60	Yuyan Chao, Lifeng He, Tsuyoshi Nakamura, Zhenghao Shi, Kenji Suzuki 0001, Hidenori Itoh	An Improvement of Herbrand's Theorem and Its Application to Model Generation Theorem Proving.	J. Comput. Sci. Technol.	2007	DBLP DOI BibTeX RDF	Herbrand’s theorem, Herbrand universe, model generation theorem proving, SATCHMO, really non-propositinal
59	Naren Narasimhan, Ranga Vemuri	On the Effectiveness of Theorem Proving Guided Discovery of Formal Assertions for a Register Allocator in a High-Level Synthesis System.	TPHOLs	1998	DBLP DOI BibTeX RDF
58	David R. Lester	Real Number Calculations and Theorem Proving.	TPHOLs	2008	DBLP DOI BibTeX RDF	Computable Reals, Exact Arithmetic, Theorem Proving, PVS, Higher-order Logic
57	Yingying Jiang 0001, Feng Tian 0001, Hongan Wang, Xiaolong Zhang 0001, XuGang Wang, Guozhong Dai	Intelligent understanding of handwritten geometry theorem proving.	IUI	2010	DBLP DOI BibTeX RDF	geometry theorem proving, hand-drawn figures, hand-written proof scripts, structure based manipulation, recognition
57	Hai Lin 0008, Jigui Sun, Yimin Zhang 0005	Theorem Proving Based on the Extension Rule.	J. Autom. Reason.	2003	DBLP DOI BibTeX RDF	extension rule, inclusion-exclusion principle, complementary factor, theorem proving
57	Gilles Dowek, Thérèse Hardin, Claude Kirchner	Theorem Proving Modulo.	J. Autom. Reason.	2003	DBLP DOI BibTeX RDF	sequent calculus modulo, resolution, rewriting, automated theorem proving, higher-order logic, cut elimination, narrowing, Skolemization, deduction modulo
57	Simon J. Gay	A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL.	TPHOLs	2001	DBLP DOI BibTeX RDF	semantics, Types, pi calculus, automatic theorem proving
56	David A. Plaisted	Special Cases and Substitutes for Rigid E-Unification.	Appl. Algebra Eng. Commun. Comput.	2000	DBLP DOI BibTeX RDF	Rigid E -unification, Theorem proving, First-order logic, Decidability, Unification, Equality, Horn clauses, Tableaux
54	Christoph Benzmüller, Andreas Meier 0002, Volker Sorge	Bridging Theorem Proving and Mathematical Knowledge Retrieval.	Mechanizing Mathematical Reasoning	2005	DBLP DOI BibTeX RDF
54	Helko Lehmann, Michael Leuschel	Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce.	LOPSTR	2003	DBLP DOI BibTeX RDF
52	Panagiotis Manolios, Daron Vroon 0001	Integrating static analysis and general-purpose theorem proving for termination analysis.	ICSE	2006	DBLP DOI BibTeX RDF	static analysis, theorem proving, termination, liveness, ACL2
52	David A. Basin, Hironobu Kuruma, Kunihiko Miyazaki, Kazuo Takaragi, Burkhart Wolff	Verifying a signature architecture: a comparative case study.	Formal Aspects Comput.	2007	DBLP DOI BibTeX RDF	Security, Model checking, Formal methods, Theorem proving, Case study, Comparison
51	Herman Geuvers, Gueorgui I. Jojgov	Open Proofs and Open Terms: A Basis for Interactive Logic.	CSL	2002	DBLP DOI BibTeX RDF	open terms, meta-variables, formulas-as-types, type theory, interactive theorem proving
51	Adel Bouhoula, Jean-Pierre Jouannaud	Automata-Driven Automated Induction.	LICS	1997	DBLP DOI BibTeX RDF	automata-driven automated induction, inductive theorem proving, first-order functions, finitely many unary membership predicates, rational subsets, ground reducibility, inductive prover, theorem proving, tree automata, Horn Clauses, proof obligations
51	Miriam Leeser, John W. O'Leary	Verification of a subtractive radix-2 square root algorithm and implementation.	ICCD	1995	DBLP DOI BibTeX RDF	subtractive radix-2 square root, floating point square root hardware, Intel Pentium, radix-2 square root, MIPS R4400, RTL level, verification, formal verification, theorem proving, theorem proving, floating point arithmetic, optimizing transformations
51	Zohar Manna, Richard J. Waldinger	Fundamentals of Deductive Program Synthesis.	IEEE Trans. Software Eng.	1992	DBLP DOI BibTeX RDF	deductive program synthesis, deductive-tableau system, theorem-proving framework, nonclausal resolution rule, induction rule, formal specification, artificial intelligence, specification, theorem proving, program testing, reasoning, inference mechanisms, proof
51	Robert E. Fields, Morten Elvang-Gøransson	A VDM Case Study in mural.	IEEE Trans. Software Eng.	1992	DBLP DOI BibTeX RDF	interactive theorem-proving assistant, specification support tool, mural, verification, formal specification, specification, software tools, theorem proving, program verification, interactive systems, VDM, Vienna development method
50	Xiao-Shan Gao, Qiang Lin	MMP/Geometer - A Software Package for Automated Geometric Reasoning.	Automated Deduction in Geometry	2002	DBLP DOI BibTeX RDF	Geometry software, geometric theorem discovering, geometric diagram generation, intelligent dynamic geometry, automated reasoning, geometric theorem proving
50	Roope Kaivola, Mark D. Aagaard	Divider Circuit Verification with Model Checking and Theorem Proving.	TPHOLs	2000	DBLP DOI BibTeX RDF
50	Marta Franová	Automated Inductive Reasoning as a Support of Deductive Reasoning in a User-Independent Automation of Inductive Theorem Proving.	ISMIS	1996	DBLP DOI BibTeX RDF
49	Michael Fisher 0001	Characterizing Simple Negotiation as Distributed Agent-Based Theorem-Proving - A Preliminary Report.	ICMAS	2000	DBLP DOI BibTeX RDF
49	Pavel Vanousek	Automated Theorem Proving in a Combination of Theories with Disjoint Signatures.	SOFSEM	1998	DBLP DOI BibTeX RDF
49	Marta Franová	Constructive Matching - Explanation Based Methodology for Inductive Theorem Proving.	IMYCS	1990	DBLP DOI BibTeX RDF
49	Larry Wos, William McCune	Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs.	CADE	1988	DBLP DOI BibTeX RDF
48	Maria Paola Bonacina	On theorem proving for program checking: historical perspective and recent developments.	PPDP	2010	DBLP DOI BibTeX RDF	combination of theories, rewrite-based theorem proving, speculative inferences, satisfiability modulo theories
48	Chiyan Chen, Hongwei Xi	Combining programming with theorem proving.	ICFP	2005	DBLP DOI BibTeX RDF	applied type system, proof erasure, theorem proving, dependent types, ATS
48	June Andronick, Boutheina Chetali, Olivier Ly	Using Coq to Verify Java Card Applet Isolation Properties.	TPHOLs	2003	DBLP DOI BibTeX RDF	Security, Theorem Proving, Smart Card
48	Harald Ganzinger, Viorica Sofronie-Stokkermans	Chaining Techniques for Automated Theorem Proving in Many-Valued Logics.	ISMVL	2000	DBLP DOI BibTeX RDF	chaining calculi, resolution, many-valued logic, automated theorem proving, superposition
48	Viorica Sofronie-Stokkermans	Representation Theorems and Theorem Proving in Non-Classical Logics.	ISMVL	1999	DBLP DOI BibTeX RDF	distributive lattices with operators, Priestley duality, many-values logics, automated theorem proving, Non-classical logics
48	Gernot Stenz, Andreas Wolf 0005	Scheduling Methods for Parallel Automated Theorem Proving.	AI	2000	DBLP DOI BibTeX RDF
47	Xia Wu, Jigui Sun, Shuai Lu 0001, Ying Li, Wei Meng, Minghao Yin	Improved Propositional Extension Rule.	RSKT	2006	DBLP DOI BibTeX RDF	Extension rule, reduced rule, theorem proving, propositional logic
47	Sigrid Gürgens, Javier López 0001	Suitability of a Classical Analysis Method for E-commerce Protocols.	ISC	2001	DBLP DOI BibTeX RDF	electronic commerce, cryptographic protocol, Security analysis, automatic theorem proving, protocol validation
47	Mark D. Aagaard, Carl-Johan H. Seger	The formal verification of a pipelined double-precision IEEE floating-point multiplier.	ICCAD	1995	DBLP DOI BibTeX RDF	ANSI/IEEE Std 754-1985, model checking, theorem proving, floating-point arithmetic, Hardware verification
47	Li Dafa	An Application to Teaching in Logic Course of ATP Based Natural Deduction.	LPAR	1992	DBLP DOI BibTeX RDF	theorem proving, logic, natural deduction
46	Anduo Wang, Prithwish Basu, Boon Thau Loo, Oleg Sokolsky	Declarative Network Verification.	PADL	2009	DBLP DOI BibTeX RDF	network protocol verification, theorem proving, domain-specific languages, Declarative networking
46	Haiyan Xiong, Paul Curzon, Sofiène Tahar, Ann Blandford	Formally Linking MDG and HOL Based on a Verified MDG System.	IFM	2002	DBLP DOI BibTeX RDF	hybrid verification systems, deductive theorem proving, symbolic state enumeration, usability verification, hardware verification
46	B. Kutzler	Careful Algebraic Translations of Geometry Theorems.	ISSAC	1989	DBLP DOI BibTeX RDF	computational analytical geometry, automated geometry theorem proving
46	César A. Muñoz, David R. Lester	Real Number Calculations and Theorem Proving.	TPHOLs	2005	DBLP DOI BibTeX RDF
46	Konrad Slind, Joe Hurd	Applications of Polytypism in Theorem Proving.	TPHOLs	2003	DBLP DOI BibTeX RDF
46	Simon Ambler, Roy L. Crole, Alberto Momigliano	Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction.	TPHOLs	2002	DBLP DOI BibTeX RDF
46	François Puitg, Jean-François Dufourd	Formal Specification and Theorem Proving Breakthroughs in Geometric Modeling.	TPHOLs	1998	DBLP DOI BibTeX RDF
45	Devrim Unal, M. Ufuk Çaglayan	Theorem proving for modeling and conflict checking of authorization policies.	ISCN	2006	DBLP DOI BibTeX RDF
45	Christian Jacobi 0002	Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving.	CAV	2002	DBLP DOI BibTeX RDF
45	Michael J. C. Gordon	PuzzleTool : An Example of Programming Computation and Deduction.	TPHOLs	2002	DBLP DOI BibTeX RDF
45	Carl-Johan H. Seger	Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice.	CADE	2000	DBLP DOI BibTeX RDF
45	Andreas Franke 0001, Michael Kohlhase	System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving.	CADE	1999	DBLP DOI BibTeX RDF
45	Anna Mikhajlova, Joakim von Wright	Proving Isomorphism of First-Order Logic Proof Systems in HOL.	TPHOLs	1998	DBLP DOI BibTeX RDF
45	Ewing L. Lusk	Controlling Redundancy in Large Search Spaces: Argonne-Style Theorem Proving Through the Years.	LPAR	1992	DBLP DOI BibTeX RDF
45	Ross A. Overbeek, Ewing L. Lusk	Data Structures and Control Architectures for Implementation of Theorem-Proving Programs.	CADE	1980	DBLP DOI BibTeX RDF
45	Larry Wos, George A. Robinson, Daniel F. Carson, Leon Shalla	The Concept of Demodulation in Theorem Proving.	J. ACM	1967	DBLP DOI BibTeX RDF
45	Ching-Tsun Chou	A Note on Interactive Theorem Proving with Theorem Continuation Functions.	TPHOLs	1992	DBLP BibTeX RDF
43	Li Dafa	Intelligent CAI Course in the First-Order Logic.	ICCAL	1990	DBLP DOI BibTeX RDF	tautology, theorem proving, first-order logic, resolution, natural deduction
43	Vlad Rusu, Eli Singerman	On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction.	TACAS	1999	DBLP DOI BibTeX RDF
42	Monty Newborn, Zongyan Wang	Octopus: Combining Learning and Parallel Search.	J. Autom. Reason.	2004	DBLP DOI BibTeX RDF	Octopus, TPTP, automated theorem proving, learning strategies, parallel search
42	Ben L. Di Vito	High-automation proofs for properties of requirements models.	Int. J. Softw. Tools Technol. Transf.	2000	DBLP DOI BibTeX RDF	Avionics software, Proof strategies, Formal methods, Theorem proving, Requirements analysis
42	Rajeev Goré, Lan Duy Nguyen	CardKt: Automated Multi-modal Deduction on Java Cards for Multi-application Security.	Java Card Workshop	2000	DBLP DOI BibTeX RDF	security of multi-application smart cards, applications of logics of knowledge and belief, modal theorem proving, tense logics
42	Andrew Ireland, Mike Jackson 0003, Gordon Reid	Interactive Proof Critics.	Formal Aspects Comput.	1999	DBLP DOI BibTeX RDF	Proof patching, Inductive proof, User interfaces, Theorem proving, Proof planning
42	Randall W. Lichota, Grace L. Hammonds, Stephen H. Brackin	Verifying The Correctness Of Cryptographic Protocols Using "Convince".	ACSAC	1996	DBLP DOI BibTeX RDF	Convince, theorem proving component, commercial computer aided software engineering tool, StP/OMT, textual notations, Higher Order Logic theorem prover, protocols, cryptographic protocols, authentication protocols, front-end, belief logic, correctness verification, automated support
42	Serge Autexier, Dieter Hutter, Bruno Langenstein, Heiko Mantel, Georg Rock, Axel Schairer, Werner Stephan 0001, Roland Vogt, Andreas Wolpers	VSE: formal methods meet industrial needs.	Int. J. Softw. Tools Technol. Transf.	2000	DBLP DOI BibTeX RDF	Formal software development, Modular proof development, Temporal logic, Compositionality, Automated theorem proving, Interactive theorem proving
42	F. Keith Hanna, Neil Daeche, Mark Longley	Specification and Verification Using Dependent Types.	IEEE Trans. Software Eng.	1990	DBLP DOI BibTeX RDF	VERITAS/sup +/, iterative structures, functional metalanguage, computational implementation, modeling, modelling, formal specification, theorem proving, theorem proving, iterative methods, dependent types, numerals, specification logic
41	Noboru Matsuda, Kurt VanLehn	Modeling Hinting Strategies for Geometry Theorem Proving.	User Modeling	2003	DBLP DOI BibTeX RDF
40	In-Hee Lee, Ji-Yoon Park, Hae-Man Jang, Young-Gyu Chai, Byoung-Tak Zhang	DNA Implementation of Theorem Proving with Resolution Refutation in Propositional Logic.	DNA	2002	DBLP DOI BibTeX RDF
40	Chad E. Brown	Solving for Set Variables in Higher-Order Theorem Proving.	CADE	2002	DBLP DOI BibTeX RDF
40	Leonardo Mendonça de Moura, Harald Rueß, Maria Sorea	Lazy Theorem Proving for Bounded Model Checking over Infinite Domains.	CADE	2002	DBLP DOI BibTeX RDF
40	Noboru Matsuda, Kurt VanLehn	A Reification of a Strategy for Geometry Theorem Proving.	Intelligent Tutoring Systems	2000	DBLP DOI BibTeX RDF
40	Panagiotis Manolios, Kedar S. Namjoshi, Robert Summers	Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation.	CAV	1999	DBLP DOI BibTeX RDF
40	Dirk Fuchs	Requirement-Based Cooperative Theorem Proving.	JELIA	1998	DBLP DOI BibTeX RDF
40	Leo Bachmair, Harald Ganzinger, Uwe Waldmann	Theorem Proving for Hierarchic First-Order Theories.	ALP	1992	DBLP DOI BibTeX RDF
40	Heikki Tuominen	Dynamic Logic as a Uniform Framework for Theorem Proving in Intensional Logic.	CADE	1990	DBLP DOI BibTeX RDF
40	David Y. Y. Yun, Y. Yun, Chang Nian Zhang	Formal verification of systolic networks using theorem proving techniques (abstract only).	ACM Conference on Computer Science	1987	DBLP DOI BibTeX RDF
40	Osman Hasan, Sofiène Tahar, Naeem Abbasi	Formal Reliability Analysis Using Theorem Proving.	IEEE Trans. Computers	2010	DBLP DOI BibTeX RDF	theorem proving, Formal models, memory structures, performance and reliability
40	Karl-Heinz Pennemann	Resolution-Like Theorem Proving for High-Level Conditions.	ICGT	2008	DBLP DOI BibTeX RDF	first-order tautology problem, high-level conditions, weak adhesive HLR categories, theorem proving, resolution
40	Steven P. Miller	Will This Be Formal?	TPHOLs	2008	DBLP DOI BibTeX RDF	model checking, Formal methods, theorem proving, avionics
40	Ghiath Al Sammane, Julien Schmaltz, Diana Toma, Pierre Ostier, Dominique Borrione	TheoSim: combining symbolic simulation and theorem proving for hardware verification.	SBCCI	2004	DBLP DOI BibTeX RDF	theorem proving, symbolic simulation, hardware verification
40	Mickaël Kerboeuf, David Nowak, Jean-Pierre Talpin	Specification and Verification of a Steam-Boiler with Signal-Coq.	TPHOLs	2000	DBLP DOI BibTeX RDF	the steam-boiler problem, theorem proving, synchronous programming
40	Keith Vanderveen, C. V. Ramamoorthy	Partial instantiation theorem proving for distributed resource location.	COMPSAC	1997	DBLP DOI BibTeX RDF	partial instantiation theorem prover, distributed resource location, INSTANT, clausal form, non clausal form, GSAT algorithm, propositional sentence, request matching, CORBA Object Trading Service, KIF, theorem proving, satisfiability, first order logic, KQML
40	David Cyrluk, Mandayam K. Srivas	Theorem proving: not an esoteric diversion, but the unifying framework for industrial verification.	ICCD	1995	DBLP DOI BibTeX RDF	industrial hardware verification, industrial verification, formal verification, logic testing, theorem proving, theorem prover, hardware verification
40	Jean H. Gallier, Paliath Narendran, Stan Raatz, Wayne Snyder	Theorem Proving Using Equational Matings and Rigid E-Unification.	J. ACM	1992	DBLP DOI BibTeX RDF	Knuth-Bendix procedure, matings, NP-completeness, unification, automated theorem proving, equational reasoning
40	Wolfgang Ertel	OR-Parallel Theorem Proving with Random Competition.	LPAR	1992	DBLP DOI BibTeX RDF	random competition, SETHEO, theorem proving, speedup, OR-parallelism, random search, model elimination
40	Oliver Bittel	Tableau-Based Theorem Proving and Synthesis of Lambda-Terms in the Intuitionistic Logic.	JELIA	1992	DBLP DOI BibTeX RDF	Typed -Calculus, Program Synthesis, Intuitionistic Logic, Automatic Theorem Proving
40	Shang-Ching Chou, Xiao-Shan Gao	Ritt-Wu's Decomposition Algorithm and Geometry Theorem Proving.	CADE	1990	DBLP DOI BibTeX RDF	Wu's method, prover, elementary geometry, degenerate conditions, Ritt-Wu's principle, ascending chain, the dimension theorem, Morley's trisector theorem, ideal, mechanical theorem proving, algebraic variety
40	Waldo C. Kabat, Anthony S. Wojcik	Automated Synthesis of Combinational Logic Using Theorem-Proving Techniques.	IEEE Trans. Computers	1985	DBLP DOI BibTeX RDF	logic design, multivalued logic, design automation, Automated theorem proving, switching theory
40	Witold S. Wojciechowski, Anthony S. Wojcik	Automated Design of Multiple-Valued Logic Circuits by Automatic Theorem Proving Techniques.	IEEE Trans. Computers	1983	DBLP DOI BibTeX RDF	multiple-valued circuits, theorem proving, logic design, first order logic, Automated design, formal proof
40	John D. McCharen, Ross A. Overbeek, Larry Wos	Problems and Experiments for and with Automated Theorem-Proving Programs.	IEEE Trans. Computers	1976	DBLP DOI BibTeX RDF	Clause sets, UR resolution, theorem-proving, resolution