Search results for "theorem-proving"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
21	Myla Archer, Constance L. Heitmeyer, Elvinia Riccobene	Using TAME to prove invariants of automata models: Two case studies.	FMSP	2000	DBLP DOI BibTeX RDF	software requirements analysis, Software engineering, verification, formal methods, theorem proving
21	Naijun Zhan	Another formal proof for Deadline Driven Scheduler.	RTCSA	2000	DBLP DOI BibTeX RDF	Deadline Driven Scheduler, DDS correctness, random preemption, induction rules, induction propositions, intuitive facts, scheduling, real-time systems, theorem proving, process algebra, duration calculus, formal proof, DC
21	Kimberly D. Voll, Tom P. Yeh, Verónica Dahl	An assumptive logic programming methodology for parsing.	ICTAI	2000	DBLP DOI BibTeX RDF	assumptive logic programming methodology, continuation based linear assumptions, timeless assumptions, datalog grammars, terse treatments, language processing phenomena, concise parser, numbered word boundaries, left-corner parsing, constituent coordination, AI, logic programming, theorem proving, DATALOG, error correction, grammars, test cases, charting, error diagnosis, proof of concept, logic grammars
21	Philippe Chatalic, Laurent Simon	Multi-resolution on compressed sets of clauses.	ICTAI	2000	DBLP DOI BibTeX RDF	compressed sets, compressed clauses, propositional clauses, compression power, structured instances, specialized operator, clause sets, polynomial size data structures, ZREs system, Davis-Putnam procedure, hard problems, SAT provers, zero-suppressed binary decision diagrams, computational complexity, data structures, data structures, data compression, theorem proving, computability, encodings, directed graphs, binary decision diagrams, set theory, multi-resolution, cut eliminations, ZBDDs
21	Clare Dixon, Michael Fisher 0001	Resolution-Based Proof for Multi-Modal Temporal Logics of Knowledge.	TIME	2000	DBLP DOI BibTeX RDF	temporal and modal logics, non-classical resolution, theorem-proving
21	Neil Evans, Steve A. Schneider	Analysing Time Dependent Security Properties in CSP Using PVS.	ESORICS	2000	DBLP DOI BibTeX RDF	Authentication Protocol Verification, Timed Behaviour, CSP, Automated Theorem Proving, PVS
21	Fiora Pirri, Raymond Reiter	Some Contributions to the Metatheory of the Situation Calculus.	J. ACM	1999	DBLP DOI BibTeX RDF	programming languages for the situation calculus, theorem-proving, regression, situation calculus
21	Wim H. Hesselink	The Verified Incremental Design of a Distributed Spanning Tree Algorithm: Extended Abstract.	Formal Aspects Comput.	1999	DBLP DOI BibTeX RDF	Message passing, Theorem proving, Minimum spanning tree, Asynchronous communication
21	Monica Nesi	Formalising a Value-Passing Calculus in HOL.	Formal Aspects Comput.	1999	DBLP DOI BibTeX RDF	Meta-theoretic reasoning, Formal verification, Theorem proving, Higher order logic, Process calculi
21	Peter Frey, Radharamanan Radhakrishnan, Philip A. Wilsey, Perry Alexander, Harold W. Carter	An Extensible Formal Framework for the Specification and Verification of an Optimistic Simulation Protocol.	HICSS	1999	DBLP DOI BibTeX RDF	Software Engineering, Theorem Proving, Parallel Discrete Event Simulation, PVS, Formal specification and verification
21	Carine Fédèle, Emmanuel Kounalis	Automatic Proofs of Properties of Simple C- Modules.	ASE	1999	DBLP DOI BibTeX RDF	inductive theorem proving, automatic proof, equational logic, Algebraic semantics
21	Philipp A. Heuberger	The minimal user interface of a simple refinement tool.	Softw. Concepts Tools	1998	DBLP DOI BibTeX RDF	Proof editing, Formal methods, Theorem proving, Refinement calculus
21	Judith Crow, Ben L. Di Vito	Formalizing Space Shuttle Software Requirements: Four Case Studies.	ACM Trans. Softw. Eng. Methodol.	1998	DBLP DOI BibTeX RDF	flight software, space shuttle, state exploration, formal methods, theorem proving, requirements analysis
21	Volker Weispfenning	Quantifier Elimination for Real Algebra - the Quadratic Case and Beyond.	Appl. Algebra Eng. Commun. Comput.	1997	DBLP DOI BibTeX RDF	Fast quantifier elimination and decision methods, First-order theory of reals, Constraint solving, Automatic theorem proving
21	Matt Kaufmann, J Strother Moore	An Industrial Strength Theorem Prover for a Logic Based on Common Lisp.	IEEE Trans. Software Eng.	1997	DBLP DOI BibTeX RDF	total functions, microcode verification, floating point division, Formal verification, digital signal processing, type checking, computational logic, automatic theorem proving, partial functions
21	William D. Young	Comparing Verification Systems: Interactive Consistency in ACL2.	IEEE Trans. Software Eng.	1997	DBLP DOI BibTeX RDF	fault tolerance, Formal verification, specification languages, computational logic, automatic theorem proving
21	Jaime Cohen, Claudio L. Lucchesi	Minimax relations for T-join packing problems.	ISTCS	1997	DBLP DOI BibTeX RDF	minimax relations, T-join packing problems, algorithmic results, structural results, minimum T-cut, maximization problem, theorem proving, polynomial time algorithm, perfect matchings, minimax techniques
21	Dan Boneh, Richard J. Lipton	Effect of Operators on Straight Line Complexity.	ISTCS	1997	DBLP DOI BibTeX RDF	straight line complexity, conditional result, explicit linear operators, lower bounds, theorem proving, multivariate polynomials
21	Susanne Graf, Hassen Saïdi	Construction of Abstract State Graphs with PVS.	CAV	1997	DBLP DOI BibTeX RDF	state graph exploration, theorem proving, abstract interpretation
21	Russ Bubley, Martin E. Dyer	Path Coupling: A Technique for Proving Rapid Mixing in Markov Chains.	FOCS	1997	DBLP DOI BibTeX RDF	P-hard counting, path coupling, combinatorial difficulty, hard combinatorial problems, TWICE-SAT, complexity, Markov chains, theorem proving, graph colouring, algorithm design, Markov chain Monte Carlo method, rapid mixing
21	Maria Luisa Bonet, Toniann Pitassi, Ran Raz	No Feasible Interpolation for TC0-Frege Proofs.	FOCS	1997	DBLP DOI BibTeX RDF	TC/sup 0/-Frege proofs, feasible interpolation, complexity-theoretic assumption, hardness assumption, lower bounds, theorem proving, Chinese Remainder Theorem, proof systems
21	Andrea Alborghetti, Angelo Gargantini, Angelo Morzenti	Providing Automated Support to Deductive Analysis of Time Critical Systems.	ESEC / SIGSOFT FSE	1997	DBLP DOI BibTeX RDF	time- and safety-critical systems, verification, formal methods, specification, temporal logic, validation, case study, automated theorem proving, experience report
21	Raul H. C. Lopes, Mark Tarver	Inducing Theorem Provers from Proofs.	ICTAI	1997	DBLP DOI BibTeX RDF	theorem prover induction, automatic theorem prover generation, proof examples, intuitionistic propositional calculus, depth-first search strategy, loop detection, inductive generalization, machine learning, theorem proving
21	Robert S. Boyer, Yuan Yu	Automated Proofs of Object Code for a Widely Used Microprocessor.	J. ACM	1996	DBLP DOI BibTeX RDF	Boyer-Moore logic, MC68xxx, Nqthm, program proving, formal methods, Ada, C, program verification, automated reasoning, Common Lisp, mechanical theorem proving, object code, machine code
21	Adel Bouhoula	General Framework for Mechanizing Induction using Test Set.	PRICAI	1996	DBLP DOI BibTeX RDF	Logic and Formal Verification, Theorem Proving, Automated reasoning
21	Stefan Gerberding	DT - An Automated Theorem Prover for Multiple-Valued First-Order Predicate Logics.	ISMVL	1996	DBLP DOI BibTeX RDF	Deep Thought, multiple-valued first-order logics, lemma generation, tableau expansion, branch closure, theorem proving, multivalued logic, multiple-valued logics, quantifiers, first-order predicate logic, truth tables, automated theorem prover
21	Hans de Nivelle	An Algorithm for the Retrieval of Unifiers from Discrimination Trees.	JELIA	1996	DBLP DOI BibTeX RDF	Algorithms, Implementation, Automated Theorem Proving
21	Manuel Enciso, Inman P. de Guzmán, Carlos Rossi	Temporal Reasoning over Linear Discrete Time.	JELIA	1996	DBLP DOI BibTeX RDF	temporal logics, automated theorem proving
21	Yves Ledru	Using KIDS as a Tool Support for VDM.	ICSE	1996	DBLP BibTeX RDF	KIDS, REGROUP, VDM specifications, correctness preserving transformations, executable prototypes synthesis, proof of consistency, formal specification, REFINE, theorem proving, program verification, specification languages, tool support, theorem prover, VDM
21	Angelika I. Kokkinaki, Kimon P. Valavanis	On the comparison of AI and DAI based planning techniques for automated manufacturing systems.	J. Intell. Robotic Syst.	1995	DBLP DOI BibTeX RDF	Planning systems, rote planning, automated manufacturing systems, learning, theorem proving, assemblies, blackboard architectures
21	Mark D. Aagaard, Miriam Leeser	Verifying a Logic-Synthesis Algorithm and Implementation: A Case Study in Software Verification.	IEEE Trans. Software Eng.	1995	DBLP DOI BibTeX RDF	weak division, theorem proving, logic synthesis, Software verification, hardware verification
21	Sam Owre, John M. Rushby, Natarajan Shankar, Friedrich W. von Henke	Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS.	IEEE Trans. Software Eng.	1995	DBLP DOI BibTeX RDF	verification systems, fault tolerance, formal specification, formal methods, theorem proving, clock synchronization, PVS, Byzantine agreement, hardware verification, flight control
21	Kenneth W. Regan, D. Sivakumar, Jin-yi Cai	Pseudorandom Generators, Measure Theory, and Natural Proofs.	FOCS	1995	DBLP DOI BibTeX RDF	natural proofs, resource-bounded measure theory, partial converse, computational complexity, theorem proving, formal languages, random number generation, measure theory, pseudorandom number generators
21	Mihir Bellare, Don Coppersmith, Johan Håstad, Marcos A. Kiwi, Madhu Sudan 0001	Linearity Testing in Characteristic Two.	FOCS	1995	DBLP DOI BibTeX RDF	characteristic two, relative distance, rejection probability, Max3SAT, MaxSNP problems, lower bounds, lower bound, probability, theorem proving, upper bound, homomorphisms, Fourier analysis, Fourier analysis, linearity testing, linear functions
21	Mihir Bellare, Oded Goldreich 0001, Madhu Sudan 0001	Free Bits, PCPs and Non-Approximability - Towards Tight Results.	FOCS	1995	DBLP DOI BibTeX RDF	free bits, logarithmic randomness, amortized free bits, Max Clique, Max-2-SAT, FGLSS connection, amortized free-bit complexity, amortized free bit complexity, FPCP parameters, triviality results, computational complexity, computational geometry, theorem proving, NP-hardness, NP complete problems, proof systems, chromatic number, PCPs, Max-cut, nonapproximability
21	Zuoquan Lin, Wei Li 0022	On Logic of Paradox.	ISMVL	1995	DBLP DOI BibTeX RDF	logic of paradox, minimal semantics, satisfactory proof theory, signed tableaux, completeness theorems, theorem proving, soundness, nonmonotonic reasoning, proof theory, paraconsistent logic, nonmonotonicity
21	Wendy MacCaull	Finite Algebraic Models for Residuated Logic.	ISMVL	1995	DBLP DOI BibTeX RDF	finite algebraic models, residuated logic, model pruning, nonclassical logics, combinatorial explosions, structure theorems, residuated algebras, theorem proving, inference mechanisms, search problems, multivalued logic, approximate reasoning, substructural logics, algebraic semantics, automated theorem prover
21	Anand Chavan, Shiu-Kai Chin, Shahid Ikram, Jang Dae Kim, Juin-Yeu Zu	Extending VLSI design with higher-order logic.	ICCD	1995	DBLP DOI BibTeX RDF	Cambridge Higher-Order Logic theorem-prover, microprogram sequencer, Am2910, VLSI, formal verification, formal verification, logic testing, theorem proving, logic design, logic CAD, VLSI design, higher-order logic, theorem-prover, design environment, instruction-set architecture, VLSI CAD
21	Volker Haarslev	Formal Semantics of Visual Languages using Spatial Reasoning.	VL	1995	DBLP DOI BibTeX RDF	qualitative spatial relationships, description logic theory, convex regions, semantics specifications, Pictorial Janus, graphical theorem proving, formal specification, visual programming, visual languages, visual languages, formal semantics, algebraic specification, spatial reasoning, spatial reasoning, points, automatic verification, lines, spatial logic, visual reasoning, geometrical objects
21	Milica Barjaktarovic, Shiu-Kai Chin, Kamal Jabbour	Formal specification and verification of communication protocols using automated tools .	ICECCS	1995	DBLP DOI BibTeX RDF	OSI protocol, large models, simulation, modelling, formal specification, formal specification, testing, protocols, formal verification, software tools, validation, theorem proving, process algebra, communication protocols, open systems, algebra, formal logic, automated tools, model checker, model testing, complex models, automated theorem prover
21	Ben C. Moszkowski	Compositional reasoning about projected and infinite time.	ICECCS	1995	DBLP DOI BibTeX RDF	multiple time granularities, parallel programming, concurrency, temporal logic, temporal logic, concurrency control, theorem proving, multiprocessing systems, deadlock, commitments, concurrent system, assumptions, Interval Temporal Logic
21	Miguel Felder, Dino Mandrioli, Angelo Morzenti	Proving Properties of Real-Time Systems Through Logical Specifications and Petri Net Models.	IEEE Trans. Software Eng.	1994	DBLP DOI BibTeX RDF	property proving, logical specifications, TRIO, Hoare method, dual language, real-time systems, real-time systems, embedded systems, formal specification, formal specification, Petri nets, temporal logic, temporal logic, theorem proving, first-order logic, timed Petri net, formal analysis, axiomatization
21	Sergio Antoy, John D. Gannon	Using Term Rewriting to Verify Software.	IEEE Trans. Software Eng.	1994	DBLP DOI BibTeX RDF	verification tasks, while statements, representation functions, generic program units, abstract base classes, algebraic axioms, Boyer-Moore prover, mechanical assistance, software tools, theorem proving, convergence, program verification, abstract data types, abstract data types, term rewriting, rewriting systems, sufficient completeness, structural induction
21	Ke Wang, Li-Yan Yuan	First-Order Logic Characterization of Program Properties.	IEEE Trans. Knowl. Data Eng.	1994	DBLP DOI BibTeX RDF	eductive databases, program properties, order reducible, FO-reducible programs, EDBs, database context, theorem-proving tools, stratified acyclic program, general chained program, bounded program, nonrecursive program, perfect models, extensional database, query processing, logic programming, logic programs, database theory, deductive databases, first-order logic, updates, integrity constraints, programming theory, fixed points, formal logic, inference rules, query answering, first-order theory
21	Belaid Benhamou, Lakhdar Sais, Pierre Siegel	Two Proof Procedures for a Cardinality Based Language in Propositional Calculus.	STACS	1994	DBLP DOI BibTeX RDF	symmetry and cardinality, theorem proving, propositional calculus
21	George K. Papakonstantinou, T. Panayiotopoulos	A full theorem-prover under uncertainty.	J. Intell. Robotic Syst.	1993	DBLP DOI BibTeX RDF	inexact reasoning, Prolog, theorem-proving, certainty, model elimination
21	David A. McAllester	Automatic Recognition of Tractability in Inference Relations.	J. ACM	1993	DBLP DOI BibTeX RDF	machine inference, theorem proving, polynomial-time algorithm, automated reasoning, inference rules, proof theory, proof systems, mechanical verification
21	David A. McAllester, Robert Givan	Taxonomic Syntax for First Order Inference.	J. ACM	1993	DBLP DOI BibTeX RDF	machine inference, theorem proving, polynomial time algorithms, automated reasoning, inference rules, proof theory, proof systems, mechanical verification
21	Robert Harper 0001, Furio Honsell, Gordon D. Plotkin	A Framework for Defining Logics.	J. ACM	1993	DBLP DOI BibTeX RDF	proof checking, interactive theorem proving, typed lambda calculus, formal systems
21	Gordon Beavers, Hal Berghel	"Dynamic" Inferencing with Generalized Resolution.	SAC	1993	DBLP DOI BibTeX RDF	automated reasoning, automated theorem proving, inferencing
21	Brendan P. Mahony, Ian J. Hayes	A Case-Study in Timed Refinement: A Mine Pump.	IEEE Trans. Software Eng.	1992	DBLP DOI BibTeX RDF	top-level refinement, simple mine pump control system, time-based systems, topologically continuous functions, discrete properties, basic building block, specification statement, refinement laws, computerized monitoring, pumps, formal specification, parallel processes, formal method, pipelined, theorem proving, mining, refinement calculus, design decisions, sequential programs, timed systems, proof of correctness
21	Peter Baumgartner 0001	An Order Theory Resolution Calculus.	LPAR	1992	DBLP DOI BibTeX RDF	Theory Resolution, Automated Theorem Proving
21	Wael M. Elseaidy	Static and dynamic analysis of real-time systems.	ACM Southeast Regional Conference	1992	DBLP DOI BibTeX RDF	SUP-INF procedure, Spec U/L bounds, deterministic timing tools, negative cycle, positive cycle, program U/L bounds, Real-time, theorem proving, real-time logic
21	Shang-Ching Chou, Xiao-Shan Gao	Proving Geometry Statements of Constructive Type.	CADE	1992	DBLP DOI BibTeX RDF	Geometry theorem proving, Wu's method, non-degenerate condition, generally true, constructive geometry statement, metric geometry, algebraically closed field, Euclidean geometry
21	Rolf Socher-Ambrosius	Boolean Algebra Admits No Convergent Term Rewriting System.	RTA	1991	DBLP DOI BibTeX RDF	Term Rewriting, Boolean Algebra, Automated Theorem Proving
21	Catherine Belleannée, Jacques Nicolas	Static Learning for an Adaptive Theorem Prover.	EWSL	1991	DBLP DOI BibTeX RDF	Key-words Theorem proving, Macro-operators, Generalization to N, Sequent calculus
21	Andrew P. Moore	The Specification and Verified Decomposition of System Requirements Using CSP.	IEEE Trans. Software Eng.	1990	DBLP DOI BibTeX RDF	verified decomposition, synchronization requirements, trace model, formal specification, formal method, specification, theorem proving, CSP, synchronisation, system requirements
21	Guo-Jie Li, Benjamin W. Wah	Computational Efficiency of Parallel Combinatorial OR-Tree Searches.	IEEE Trans. Software Eng.	1990	DBLP DOI BibTeX RDF	near linear speedup, parallel combinatorial OR-tree searches, error allowance function, simulation, performance evaluation, performance, parallel processing, theorem proving, database management systems, trees (mathematics), decision theory, sufficient conditions, search strategies, combinatorial mathematics, dominance relation
21	David M. Goldschlag	Mechanically Verifying Concurrent Programs with the Boyer-Moore Prover.	IEEE Trans. Software Eng.	1990	DBLP DOI BibTeX RDF	mechanically verifying concurrent programs, Boyer-Moore prover, transition system model, parallel programming, distributed algorithm, concurrency, theorem proving, program verification, safety, encoding, encoding, operational semantics, inference mechanisms, liveness, inference rules, proof system, Unity
21	Albert John Camilleri	Mechanizing CSP Trace Theory in Higher Order Logic.	IEEE Trans. Software Eng.	1990	DBLP DOI BibTeX RDF	mechanising CSP trace theory, general-purpose theorem prover, formal specification, theorem proving, formal logic, higher order logic, communicating sequential processes
21	Christian B. Suttner, Wolfgang Ertel	Automatic Acquisition of Search Guiding Heuristics.	CADE	1990	DBLP DOI BibTeX RDF	learning, heuristics, features, Automated theorem proving, back-propagation, connectionism, evaluation functions, model elimination
21	Johann Schumann, Reinhold Letz	PARTHEO: A High-Performance Parallel Theorem Prover.	CADE	1990	DBLP DOI BibTeX RDF	Warren Abstract Machine, message passing, Theorem proving, first-order logic, transputers, or-parallelism, model elimination, connection method
21	Ricardo Caferra, Nicolas Zabel	Extending Resolution for Model Construction.	JELIA	1990	DBLP DOI BibTeX RDF	Equational Problems, Disunification, Theorem Proving, Decision Procedures, Unification, Model Construction
21	Dipankar Sarkar 0001, S. C. De Sarkar	A Theorem Prover for Verifying Iterative Programs Over Integers.	IEEE Trans. Software Eng.	1989	DBLP DOI BibTeX RDF	rule-based theorem prover, iterative programs, overall proof construction strategy, array-sorting program, expert systems, theorem proving, program verification, performance measures, iterative methods, correctness proofs
21	Dipankar Sarkar 0001, S. C. De Sarkar	Some Inference Rules for Integer Arithmetic for Verification of Flowchart Programs on Integers.	IEEE Trans. Software Eng.	1989	DBLP DOI BibTeX RDF	flowchart programs, first-order rules, algebraic expressions, proof construction process, human thought process, user provided axioms, verification, theorem proving, program verification, inference mechanisms, inference rules, theorem prover, integer arithmetic
21	George Peterka, Tadao Murata	Proof Procedure and Answer Extraction in Petri Net Model of Logic Programs.	IEEE Trans. Software Eng.	1989	DBLP DOI BibTeX RDF	proof procedure, Horn clause subset, firing sequence, goal transition, Petri nets, logic programs, logic programming, theorem proving, programming theory, Petri net model, first-order predicate logic, answer extraction
21	William R. Bevier	Kit: A Study in Operating System Verification.	IEEE Trans. Software Eng.	1989	DBLP DOI BibTeX RDF	multitasking operating system kernel, machine language, uniprocessor von Neumann computer, conceptually distributed communicating processes, asynchronous devices, security-related results, supervisor mode, Boyer-Moore logic, Boyer-Moore theorem prover, verification, interface, message passing, theorem proving, program verification, operating systems (computers), multiprogramming, correctness proof, process scheduling, error handling, Kit
21	Dipankar Sarkar 0001, S. C. De Sarkar	A Set of Inference Rules for Quantified Formula Handling and Array Handling in Verification of Programs Over Integers.	IEEE Trans. Software Eng.	1989	DBLP DOI BibTeX RDF	quantified formula handling, array handling, undecidability problem, automated verifier, quantified formulas, bound-extension rule, bound-modification, theorem proving, program verification, program verification, first-order logic, inference mechanisms, decidability, inference rules, integer arithmetic
21	Jeffrey J. Joyce	Totally Verified Systems: Linking Verified Software to Verified Hardware.	Hardware Specification, Verification and Synthesis	1989	DBLP DOI BibTeX RDF	machine-assisted theorem proving, safety-critical systems, higher-order logic, hardware verification, compiler correctness
21	Uwe Petermann	An Extended Herbrand Theorem for First-Order Theories with Equality Interpreted in Partial Algebras.	MFCS	1989	DBLP DOI BibTeX RDF	Herbrand Disjunctions, Built in Theories, Theorem Proving, Partial Algebras, Connection Method
21	Tobias Nipkow	Formal Verification of Data Type Refinement - Theory and Practice.	REX Workshop	1989	DBLP DOI BibTeX RDF	Verification, Distributed Processes, Refinement, Implementation, Theorem Proving, Abstract Data Types, Data Types
21	Hans Jürgen Ohlbach	New Ways for Developing Proof Theories for First-Order Multi Modal Logics.	CSL	1989	DBLP DOI BibTeX RDF	Automated Theorem Proving by Translation and Refutation, Nonclassical Logics, Process Logic, Action Logic, Temporal Logic, Modal Logic, Resolution, Epistemic Logic
21	Werner Damm	A Microprogramming Logic.	IEEE Trans. Software Eng.	1988	DBLP DOI BibTeX RDF	microprogramming logic, syntax-directed proof system, horizontal computer architectures, clocked microarchitectures, axiomatic definition, microoperations, low-level parallelism, dynamic conflicts, specification, computer architecture, theorem proving, specification languages, architecture description language, formal logic, microprogramming, AADL, timing behavior
21	David A. Basin	An Environment For Automated Reasoning About Partial Functions.	CADE	1988	DBLP DOI BibTeX RDF	Automated program development, unsolvability, theorem proving, computability, type theory, constructivity, tactics, partial functions
21	Ilkka Niemelä	Decision Procedure for Autoepistemic Logic.	CADE	1988	DBLP DOI BibTeX RDF	analytic tableaux, theorem proving, Nonmonotonic logic
21	Arkady Rabinov	A Restriction of Factoring in Binary Resolution.	CADE	1988	DBLP DOI BibTeX RDF	binary resolution, theorem proving, Factoring
21	Bill Pase, Sentot Kromodimoeljo	m-NEVER System Summary.	CADE	1988	DBLP DOI BibTeX RDF	Automatic induction, forward rules, program verification, decision procedures, interactive theorem proving, rewrite rules
21	Roderic A. Girle, Michael A. McRobbie	Exploring the Epistemic Labyrinth: New Directions in the Formal Theory of Knowledge Representation.	Australian Joint Conference on Artificial Intelligence	1988	DBLP DOI BibTeX RDF	knowledge representation, modal logics, automated theorem proving, multi-valued logics
21	Vijay Pitchumani, Edward P. Stabler	An Inductive Assertion Method for Register Transfer Level Design Verification.	IEEE Trans. Computers	1983	DBLP DOI BibTeX RDF	inductive assertion method, synchronous logic, theorem proving, Assertions, predicate calculus, register transfer level design, verification condition
21	Paul Y. Gloess, Jean-Pierre H. Laurent	Adding Dynamic Paramodulation to Rewrite Algorithms.	CADE	1980	DBLP DOI BibTeX RDF	critical pairs, Knuth-Bendix algorithm, paramodulation, rewrite algorithms, theorem-proving, rewrite rules
21	Alan Bundy, Bob Welham	Using Meta-Level Inference for Selective Application of Multiple Rewrite Rules in Algebraic Manipulation.	CADE	1980	DBLP DOI BibTeX RDF	mathematical reasoning, algebraic manipulation and meta-level reasoning, theorem proving, rewrite rules
21	Helga Noll	A Note on Resolution: How to Get Rid of Factoring without Loosing Completeness.	CADE	1980	DBLP DOI BibTeX RDF	theorem proving, factoring, first order logic, resolution
21	Walter Maner	Curriculum generators: Some design problems.	ACM Annual Conference (2)	1978	DBLP DOI BibTeX RDF	Technology and man, Artificial intelligence, Theorem-proving, Logic, Problem-solving, Cognition, Curriculum development, Heuristic methods, Computer- assisted instruction
21	Gerald A. Wilson, Jack Minker	Resolution, Refinements, and Search Strategies: A Comparative Study.	IEEE Trans. Computers	1976	DBLP DOI BibTeX RDF	linear resolution, P1 resolution, proof procedure system, Q* algorithm, resolution inference, set of support resolution, ?* algorithm, SL resolution, theorem proving, problem solving, search strategies, Comparative analysis
21	Robert C. Moore	D-Script: A Computational Theory of Descriptions.	IEEE Trans. Computers	1976	DBLP DOI BibTeX RDF	Knowledge about knowledge, opaque contexts, representation of knowledge, time contexts, theorem proving, natural language understanding
21	Erik Sandewall	Conversion of Predicate-Calculus Axioms to Corresponding Deterministic Programs.	IEEE Trans. Computers	1976	DBLP DOI BibTeX RDF	FUNARG-expression, nondeterministic, theorem proving, retrieval, Closure, deduction
21	David Gelperin	A Resolution-Based Proof Procedure Using Deletion-Directed Search.	IEEE Trans. Computers	1976	DBLP DOI BibTeX RDF	clause deletion, deletion-directed search, mate tables, heuristic search, resolution, formal logic, Automatic theorem proving
21	Peter B. Andrews	Refutations by Matings.	IEEE Trans. Computers	1976	DBLP DOI BibTeX RDF	clause-occurrence, mating, unsatisfiability, first-order logic, resolution, merge, cycle, Automatic theorem proving, refutation
21	George W. Ernst, Raymond J. Hookway	The Use of Higher Order Logic in Program Verification.	IEEE Trans. Computers	1976	DBLP DOI BibTeX RDF	inductive assertions, program verification, Heuristic search, higher order logic, mechanical theorem proving
21	George W. Ernst	A Definition-Driven Theorem Prover.	IEEE Trans. Computers	1976	DBLP DOI BibTeX RDF	natural deduction systems, Artificial intelligence, heuristic search, higher order logic, mechanical theorem proving
21	Robert S. Boyer, J Strother Moore, Robert E. Shostak	Primitive Recursive Program Transformations.	POPL	1976	DBLP DOI BibTeX RDF	Theorem proving, Program verification, LISP, LISP, Flowcharts, Structural induction
20	Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz 0001	New results on rewrite-based satisfiability procedures.	ACM Trans. Comput. Log.	2009	DBLP DOI BibTeX RDF	combination of theories, satisfiability modulo a theory, scalability, inference, termination, Automated reasoning, decision procedures, rewriting, superposition
20	Jörg H. Siekmann, Christoph Benzmüller, Armin Fiedler, Andreas Meier 0002, Martin Pollet	Proof Development with Omega-MEGA: sqrt(2) Is Irrational.	LPAR	2002	DBLP DOI BibTeX RDF
20	Deepak Kapur, Mahadevan Subramaniam	Using an induction prover for verifying arithmetic circuits.	Int. J. Softw. Tools Technol. Transf.	2000	DBLP DOI BibTeX RDF	Induction, Automated reasoning, Decision procedures, Rewriting, Arithmetic circuits, Hardware verification
20	Predrag Janicic, Alan Bundy, Ian Green	A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers.	CADE	1999	DBLP DOI BibTeX RDF
19	Dang Duy Bui, Duong Dinh Tran, Kazuhiro Ogata 0001, Adrián Riesco 0001	Integration of state machine graphical animation and Maude to facilitate characteristic conjecture: an approach to lemma discovery in theorem proving.	Multim. Tools Appl.	2024	DBLP DOI BibTeX RDF
19	Jason Rute, Miroslav Olsák, Lasse Blaauwbroek, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, Vasily Pestun	Graph2Tac: Learning Hierarchical Representations of Math Concepts in Theorem proving.	CoRR	2024	DBLP DOI BibTeX RDF
19	Sean Lamont, Michael Norrish, Amir Dezfouli, Christian Walder, Paul Montague	BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving.	CoRR	2024	DBLP DOI BibTeX RDF
19	Andreas Florath	Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code.	CoRR	2024	DBLP DOI BibTeX RDF
19	Sean Lamont, Michael Norrish, Amir Dezfouli, Christian Walder, Paul Montague	BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving.	AAAI	2024	DBLP DOI BibTeX RDF