|
|
Venues (Conferences, Journals, ...)
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
The graphs summarize 1960 occurrences of 846 keywords
|
|
|
Results
Found 3383 publication records. Showing 3383 according to the selection in the facets
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMSP ![In: Proceedings of the Third Workshop on Formal Methods in Software Practice, 2000, Portland, Oregon, USA, pp. 25-36, 2000, ACM, 1-58113-262-X. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTCSA ![In: 7th International Workshop on Real-Time Computing and Applications Symposium (RTCSA 2000), 12-14 December 2000, Cheju Island, South Korea, pp. 481-485, 2000, IEEE Computer Society, 0-7695-0930-4. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICTAI ![In: 12th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2000), 13-15 November 2000, Vancouver, BC, Canada, pp. 11-18, 2000, IEEE Computer Society, 0-7695-0909-6. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICTAI ![In: 12th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2000), 13-15 November 2000, Vancouver, BC, Canada, pp. 2-10, 2000, IEEE Computer Society, 0-7695-0909-6. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TIME ![In: Seventh International Workshop on Temporal Representation and Reasoning, TIME 2000, Nova Scotia, Canada, July 7-9, 2000, pp. 69-78, 2000, IEEE Computer Society, 0-7695-0756-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ESORICS ![In: Computer Security - ESORICS 2000, 6th European Symposium on Research in Computer Security, Toulouse, France, October 4-6, 2000, Proceedings, pp. 222-237, 2000, Springer, 3-540-41031-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. ACM ![In: J. ACM 46(3), pp. 325-361, 1999. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 11(1), pp. 45-55, 1999. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
Message passing, Theorem proving, Minimum spanning tree, Asynchronous communication |
21 | Monica Nesi |
Formalising a Value-Passing Calculus in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 11(2), pp. 160-199, 1999. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
HICSS ![In: 32nd Annual Hawaii International Conference on System Sciences (HICSS-32), January 5-8, 1999, Maui, Hawaii, USA, 1999, IEEE Computer Society, 0-7695-0001-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ASE ![In: The 14th IEEE International Conference on Automated Software Engineering, ASE 1999, Cocoa Beach, Florida, USA, 12-15 October 1999, pp. 283-286, 1999, IEEE Computer Society, 0-7695-0415-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Softw. Concepts Tools ![In: Softw. Concepts Tools 19(2), pp. 89-95, 1998. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Softw. Eng. Methodol. ![In: ACM Trans. Softw. Eng. Methodol. 7(3), pp. 296-332, 1998. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Appl. Algebra Eng. Commun. Comput. ![In: Appl. Algebra Eng. Commun. Comput. 8(2), pp. 85-101, 1997. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 23(4), pp. 203-213, 1997. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 23(4), pp. 214-223, 1997. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISTCS ![In: Fifth Israel Symposium on Theory of Computing and Systems, ISTCS 1997, Ramat-Gan, Israel, June 17-19, 1997, Proceedings, pp. 38-44, 1997, IEEE Computer Society, 0-8186-8037-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISTCS ![In: Fifth Israel Symposium on Theory of Computing and Systems, ISTCS 1997, Ramat-Gan, Israel, June 17-19, 1997, Proceedings, pp. 1-5, 1997, IEEE Computer Society, 0-8186-8037-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 9th International Conference, CAV '97, Haifa, Israel, June 22-25, 1997, Proceedings, pp. 72-83, 1997, Springer, 3-540-63166-6. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FOCS ![In: 38th Annual Symposium on Foundations of Computer Science, FOCS '97, Miami Beach, Florida, USA, October 19-22, 1997, pp. 223-231, 1997, IEEE Computer Society, 0-8186-8197-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FOCS ![In: 38th Annual Symposium on Foundations of Computer Science, FOCS '97, Miami Beach, Florida, USA, October 19-22, 1997, pp. 254-263, 1997, IEEE Computer Society, 0-8186-8197-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ESEC / SIGSOFT FSE ![In: Software Engineering - ESEC/FSE '97, 6th European Software Engineering Conference Held Jointly with the 5th ACM SIGSOFT Symposium on Foundations of Software Engineering, Zurich, Switzerland, September 22-25, 1997, Proceedings, pp. 211-226, 1997, Springer, 3-540-63531-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICTAI ![In: 9th International Conference on Tools with Artificial Intelligence, ICTAI '97, Newport Beach, CA, USA, November 3-8, 1997, pp. 157-164, 1997, IEEE Computer Society, 0-8186-8203-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. ACM ![In: J. ACM 43(1), pp. 166-192, 1996. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PRICAI ![In: PRICAI'96: Topics in Artificial Intelligence, 4th Pacific Rim International Conference on Artificial Intelligence, Cairns, Australia, August 26-30, 1996, Proceedings, pp. 1-12, 1996, Springer, 3-540-61532-6. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISMVL ![In: 26th IEEE International Symposium on Multiple-Valued Logic, ISMVL 1996, Santiago de Compostela, Spain, May 29-31, 1996, Proceedings, pp. 284-289, 1996, IEEE Computer Society, 0-8186-7392-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
JELIA ![In: Logics in Artificial Intelligence, European Workshop, JELIA '96, Évora, Portugal, September 30 - October 3, 1996, Proceedings, pp. 18-33, 1996, Springer, 3-540-61630-6. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
JELIA ![In: Logics in Artificial Intelligence, European Workshop, JELIA '96, Évora, Portugal, September 30 - October 3, 1996, Proceedings, pp. 303-319, 1996, Springer, 3-540-61630-6. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
temporal logics, automated theorem proving |
21 | Yves Ledru |
Using KIDS as a Tool Support for VDM. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICSE ![In: 18th International Conference on Software Engineering, Berlin, Germany, March 25-29, 1996, Proceedings., pp. 236-245, 1996, IEEE Computer Society, 0-8186-7246-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Intell. Robotic Syst. ![In: J. Intell. Robotic Syst. 13(3), pp. 201-245, 1995. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 21(10), pp. 822-833, 1995. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 21(2), pp. 107-125, 1995. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FOCS ![In: 36th Annual Symposium on Foundations of Computer Science, Milwaukee, Wisconsin, USA, 23-25 October 1995, pp. 26-35, 1995, IEEE Computer Society, 0-8186-7183-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FOCS ![In: 36th Annual Symposium on Foundations of Computer Science, Milwaukee, Wisconsin, USA, 23-25 October 1995, pp. 432-441, 1995, IEEE Computer Society, 0-8186-7183-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FOCS ![In: 36th Annual Symposium on Foundations of Computer Science, Milwaukee, Wisconsin, USA, 23-25 October 1995, pp. 422-431, 1995, IEEE Computer Society, 0-8186-7183-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISMVL ![In: 25th IEEE International Symposium on Multiple-Valued Logic, ISMVL 1995, Bloomington, Indiana, USA, May 23-25, 1995, Proceedings, pp. 248-255, 1995, IEEE Computer Society, 0-8186-7118-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISMVL ![In: 25th IEEE International Symposium on Multiple-Valued Logic, ISMVL 1995, Bloomington, Indiana, USA, May 23-25, 1995, Proceedings, pp. 206-215, 1995, IEEE Computer Society, 0-8186-7118-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICCD ![In: 1995 International Conference on Computer Design (ICCD '95), VLSI in Computers and Processors, October 2-4, 1995, Austin, TX, USA, Proceedings, pp. 85-94, 1995, IEEE Computer Society, 0-8186-7165-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
VL ![In: Proceedings 11th International IEEE Symposium on Visual Languages, Darmstadt, Germany, September 5-9, 1995, pp. 156-163, 1995, IEEE Computer Society, 0-8186-7045-2. The full citation details ...](Pics/full.jpeg) |
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 . ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICECCS ![In: 1st IEEE International Conference on Engineering of Complex Computer Systems (ICECCS '95), November 6-10, 1995, Fort Lauderdale, Florida, USA, pp. 246-253, 1995, IEEE Computer Society, 0-8186-7123-8. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICECCS ![In: 1st IEEE International Conference on Engineering of Complex Computer Systems (ICECCS '95), November 6-10, 1995, Fort Lauderdale, Florida, USA, pp. 238-245, 1995, IEEE Computer Society, 0-8186-7123-8. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 20(2), pp. 127-141, 1994. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 20(4), pp. 259-274, 1994. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Knowl. Data Eng. ![In: IEEE Trans. Knowl. Data Eng. 6(4), pp. 518-533, 1994. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
STACS ![In: STACS 94, 11th Annual Symposium on Theoretical Aspects of Computer Science, Caen, France, February 24-26, 1994, Proceedings, pp. 71-82, 1994, Springer, 3-540-57785-8. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
symmetry and cardinality, theorem proving, propositional calculus |
21 | George K. Papakonstantinou, T. Panayiotopoulos |
A full theorem-prover under uncertainty. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Intell. Robotic Syst. ![In: J. Intell. Robotic Syst. 7(2), pp. 139-149, 1993. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
inexact reasoning, Prolog, theorem-proving, certainty, model elimination |
21 | David A. McAllester |
Automatic Recognition of Tractability in Inference Relations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. ACM ![In: J. ACM 40(2), pp. 284-303, 1993. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. ACM ![In: J. ACM 40(2), pp. 246-283, 1993. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. ACM ![In: J. ACM 40(1), pp. 143-184, 1993. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SAC ![In: Proceedings of the 1993 ACM/SIGAPP Symposium on Applied Computing: States of the Art and Practice, SAC'93, Indianapolis, IN, USA, February 14-16, 1993, pp. 614-621, 1993, ACM, 0-89791-567-4. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 18(9), pp. 817-826, 1992. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic Programming and Automated Reasoning,International Conference LPAR'92, St. Petersburg, Russia, July 15-20, 1992, Proceedings, pp. 119-130, 1992, Springer, 3-540-55727-X. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
Theory Resolution, Automated Theorem Proving |
21 | Wael M. Elseaidy |
Static and dynamic analysis of real-time systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Southeast Regional Conference ![In: Proceedings of the 30th Annual Southeast Regional Conference, 1992, Raleigh, North Carolina, USA, April 8-10, 1992, pp. 368-376, 1992, ACM, 0-89791-506-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings, pp. 20-34, 1992, Springer, 3-540-55602-8. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, 4th International Conference, RTA-91, Como, Italy, April 10-12, 1991, Proceedings, pp. 264-274, 1991, Springer, 3-540-53904-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
EWSL ![In: Machine Learning - EWSL-91, European Working Session on Learning, Porto, Portugal, March 6-8, 1991, Proceedings, pp. 298-311, 1991, Springer, 3-540-53816-X. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 16(9), pp. 932-948, 1990. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 16(1), pp. 13-31, 1990. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 16(9), pp. 1005-1023, 1990. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 16(9), pp. 993-1004, 1990. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, pp. 470-484, 1990, Springer, 3-540-52885-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, pp. 40-56, 1990, Springer, 3-540-52885-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
JELIA ![In: Logics in AI, European Workshop, JELIA '90, Amsterdam, The Netherlands, September 10-14, 1990, Proceedings, pp. 153-169, 1990, Springer, 3-540-53686-8. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 15(12), pp. 1550-1566, 1989. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 15(1), pp. 1-9, 1989. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 15(2), pp. 209-217, 1989. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 15(11), pp. 1382-1396, 1989. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 15(11), pp. 1368-1381, 1989. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Hardware Specification, Verification and Synthesis ![In: Hardware Specification, Verification and Synthesis: Mathematical Aspects, Mathematical Science Institute Workshop, Cornall University, Ithaca, New York, USA, July 5-7, 1989, Proceedings, pp. 177-201, 1989, Springer, 3-540-97226-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MFCS ![In: Mathematical Foundations of Computer Science 1989, MFCS'89, Porabka-Kozubnik, Poland, August 28 - September 1, 1989, Proceedings, pp. 408-417, 1989, Springer, 3-540-51486-4. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
REX Workshop ![In: Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, REX Workshop, Mook, The Netherlands, May 29 - June 2, 1989, Proceedings, pp. 561-591, 1989, Springer, 3-540-52559-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSL ![In: CSL '89, 3rd Workshop on Computer Science Logic, Kaiserslautern, Germany, October 2-6, 1989, Proceedings, pp. 271-308, 1989, Springer, 3-540-52753-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 14(5), pp. 559-574, 1988. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings, pp. 101-110, 1988, Springer, 3-540-19343-X. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings, pp. 675-684, 1988, Springer, 3-540-19343-X. The full citation details ...](Pics/full.jpeg) |
1988 |
DBLP DOI BibTeX RDF |
analytic tableaux, theorem proving, Nonmonotonic logic |
21 | Arkady Rabinov |
A Restriction of Factoring in Binary Resolution. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings, pp. 582-591, 1988, Springer, 3-540-19343-X. The full citation details ...](Pics/full.jpeg) |
1988 |
DBLP DOI BibTeX RDF |
binary resolution, theorem proving, Factoring |
21 | Bill Pase, Sentot Kromodimoeljo |
m-NEVER System Summary. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings, pp. 738-739, 1988, Springer, 3-540-19343-X. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Australian Joint Conference on Artificial Intelligence ![In: AI '88: 2nd Australian Joint Artificial Intelligence Conference, Adelaide, Australia, November 15-18, 1988, Proceedings, pp. 156-176, 1988, Springer, 3-540-52062-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Computers ![In: IEEE Trans. Computers 32(12), pp. 1073-1080, 1983. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 5th Conference on Automated Deduction, Les Arcs, France, July 8-11, 1980, Proceedings, pp. 195-207, 1980, Springer, 3-540-10009-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 5th Conference on Automated Deduction, Les Arcs, France, July 8-11, 1980, Proceedings, pp. 24-38, 1980, Springer, 3-540-10009-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 5th Conference on Automated Deduction, Les Arcs, France, July 8-11, 1980, Proceedings, pp. 250-263, 1980, Springer, 3-540-10009-1. The full citation details ...](Pics/full.jpeg) |
1980 |
DBLP DOI BibTeX RDF |
theorem proving, factoring, first order logic, resolution |
21 | Walter Maner |
Curriculum generators: Some design problems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Annual Conference (2) ![In: Proceedings 1978 ACM Annual Conference, Washington, DC, USA, December 4-6, 1978, Volume II, pp. 753-758, 1978, ACM, 978-0-89791-000-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Computers ![In: IEEE Trans. Computers 25(8), pp. 782-801, 1976. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Computers ![In: IEEE Trans. Computers 25(4), pp. 366-373, 1976. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Computers ![In: IEEE Trans. Computers 25(4), pp. 342-346, 1976. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Computers ![In: IEEE Trans. Computers 25(4), pp. 323-327, 1976. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Computers ![In: IEEE Trans. Computers 25(8), pp. 801-807, 1976. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Computers ![In: IEEE Trans. Computers 25(8), pp. 844-851, 1976. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Computers ![In: IEEE Trans. Computers 25(4), pp. 317-322, 1976. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Conference Record of the Third ACM Symposium on Principles of Programming Languages, Atlanta, Georgia, USA, January 1976, pp. 171-174, 1976, ACM Press. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Comput. Log. ![In: ACM Trans. Comput. Log. 10(1), pp. 4:1-4:51, 2009. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 9th International Conference, LPAR 2002, Tbilisi, Georgia, October 14-18, 2002, Proceedings, pp. 367-387, 2002, Springer, 3-540-00010-0. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
20 | Deepak Kapur, Mahadevan Subramaniam |
Using an induction prover for verifying arithmetic circuits. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 3(1), pp. 32-65, 2000. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, pp. 127-141, 1999, Springer, 3-540-66222-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Multim. Tools Appl. ![In: Multim. Tools Appl. 83(12), pp. 36865-36898, April 2024. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2401.02949, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP DOI BibTeX RDF |
|
19 | Sean Lamont, Michael Norrish, Amir Dezfouli, Christian Walder, Paul Montague |
BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2403.03401, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP DOI BibTeX RDF |
|
19 | Andreas Florath |
Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2403.12627, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP DOI BibTeX RDF |
|
19 | Sean Lamont, Michael Norrish, Amir Dezfouli, Christian Walder, Paul Montague |
BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AAAI ![In: Thirty-Eighth AAAI Conference on Artificial Intelligence, AAAI 2024, Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence, IAAI 2024, Fourteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2014, February 20-27, 2024, Vancouver, Canada, pp. 10607-10615, 2024, AAAI Press. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP DOI BibTeX RDF |
|
Displaying result #501 - #600 of 3383 (100 per page; Change: ) Pages: [ <<][ 1][ 2][ 3][ 4][ 5][ 6][ 7][ 8][ 9][ 10][ 11][ 12][ 13][ 14][ 15][ >>] |
|