Search results for "J. Autom. Reasoning"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
1	C. A. Johnson	Computing Only Minimal Answers in Disjunctive Deductive Databases.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Disjunctive deductive databases, Minimal answers, Perfect models, Disjunctive stable models, Cyclic sets, Strong covers, Database pre-processing, Compilation
1	Marko Samer, Stefan Szeider	Backdoor Sets of Quantified Boolean Formulas.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Backdoor sets, Variable dependencies, Parameterized complexity, Quantified Boolean formulas
1	Magnus Björk	First Order Stålmarck.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Stålmarck’s method, Universal lemmas, First order logic, Automated theorem proving, Intersections
1	Osman Hasan, Sofiène Tahar	Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	HOL theorem prover, Real-time systems, Communication protocols, Higher-order-logic, Probability theory
1	María-del-Mar Gallardo, Pedro Merino, David Sanán	Model Checking Dynamic Memory Allocation in Operating Systems.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Model checking, Operating systems, Dynamic memory allocation
1	Harvey Tuch	Formal Verification of C Systems Code.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	C, Separation logic, Interactive theorem proving
1	Gerwin Klein, Ralf Huuck, Bastian Schlich	Operating System Verification.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF
1	Syrine Tlili, Mourad Debbabi	Interprocedural and Flow-Sensitive Type Analysis for Memory and Type Safety of C Code.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Type and effect analysis, C language, Type safety, Memory safety
1	Xinyu Feng, Zhong Shao, Yu Guo, Yuan Dong	Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Operating system verification, Hardware interrupts, Preemptive threads, Thread libraries, Modularity, Separation logic, Synchronization primitives
1	Hendrik Tews, Marcus Völp, Tjark Weber	Formal Memory Models for the Verification of Low-Level Operating-System Code.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Micro-hypervisor, Memory-mapped devices, Formal verification, Virtual memory, Operating-system kernel
1	Matthias Daum, Jan Dörrenbächer, Burkhart Wolff	Proving Fairness and Implementation Correctness of a Microkernel Scheduler.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Formal verification, Interactive theorem proving, Microkernel, Isabelle/HOL
1	Eyad Alkassar, Mark A. Hillebrand, Dirk Leinenbach, Norbert Schirmer, Artem Starostin, Alexandra Tsyban	Balancing the Load.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Pervasive formal verification, Software verification, Systems verification
1	Filip Maric	Formalization and Implementation of Modern SAT Solvers.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Algorithms, Data structures, Software verification, DPLL, SAT solving
1	Harald Zankl, Nao Hirokawa, Aart Middeldorp	KBO Orientability.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Knuth-Bendix order, Termination, Term rewriting
1	Giorgio Dalzotto, Tomás Recio	On Protocols for the Automated Discovery of Theorems in Elementary Geometry.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Automatic theorem discovery, Elementary geometry, Computational algebraic geometry, Automatic theorem proving
1	Raul Monroy, Alan Bundy, Ian Green	On Process Equivalence = Equation Solving in CCS.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Unique fixpoint induction, Equational verification Calculus of communicating systems
1	K. Subramani	Optimal Length Resolution Refutations of Difference Constraint Systems.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Difference constraint systems, Resolution refutation, Optimal length, Minimum unsatisfiable subset, Fourier-Motzkin elimination
1	Jean-François Dufourd	An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Computer-aided proofs, Coq system, Planar subdivisions, Combinatorial hypermaps, Discrete Jordan Curve Theorem, Formal specifications, Computational topology
1	Ruben A. Gamboa	A Formalization of Powerlist Algebra in ACL2.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Powerlists, Verification, ACL2
1	Jasmin Christian Blanchette	Proof Pearl: Mechanizing the Textbook Proof of Huffman's Algorithm.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Interactive theorem provers, Huffman coding, Higher-order logic
1	Marc Bezem, Dimitri Hendriks	On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Coherent logic, Proof objects, Hessenberg’s theorem, Automated theorem proving
1	Jia Meng, Lawrence C. Paulson	Translating Higher-Order Clauses to First-Order Clauses.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Interactive theorem provers, Clause translation, First-order logic, Higher-order logic
1	Mark H. Liffiton, Karem A. Sakallah	Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Minimal unsatifiable subset, CAMUS, Constraint satisfaction
1	Ulrich Furbach	IJCAR Preface.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF
1	Laurence Rideau, Bernard P. Serpette, Xavier Leroy	Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Parallel move, Parallel assignment, The Coq proof assistant, Compilation, Compiler correctness
1	Kaustuv Chaudhuri, Frank Pfenning, Greg Price	A Logical Characterization of Forward and Backward Chaining in the Inverse Method.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	SLD resolution, Hyperresolution, Intuitionistic linear logic, Focusing, Inverse method
1	Bishop Brock, Matt Kaufmann, J. Strother Moore	Rewriting with Equivalence Relations in ACL2.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Refinement, Rewriting, Congruence, Equivalence relations
1	Yevgeny Kazakov, Boris Motik	A Resolution-Based Decision Procedure for SHOIQ.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF
1	Andrey Paskevich	Connection Tableaux with Lazy Paramodulation.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Connection tableaux, Lazy paramodulation, Basic ordered paramodulation, First-order logic with equality
1	Jörg Endrullis, Johannes Waldmann, Hans Zantema	Matrix Interpretations for Proving Termination of Term Rewriting.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Matrix interpretations, Satisfiability, Termination, Term rewriting
1	David Toman, Grant E. Weddell	On Keys and Functional Dependencies as First-Class Citizens in Description Logics.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Path-functional dependency, Relational keys, Description logics
1	Sandip Ray, Warren A. Hunt Jr., John Matthews, J. Strother Moore	A Mechanical Analysis of Program Verification Strategies.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Inductive assertions, Partial correctness, Theorem proving, Invariants, Total correctness
1	Volker Sorge, Andreas Meier, Roy L. McCasland, Simon Colton	Automatic Construction and Verification of Isotopy Invariants.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Automated mathematics, Classification theorems, Computer algebra, Automated theorem proving, Model generation, Invariant generation, SAT solving, Isotopy
1	Christian Urban	Nominal Techniques in Isabelle/HOL.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Nominal logic work, Lambda-calculus, Theorem provers
1	Jesús Aransay, Clemens Ballarin, Julio Rubio	A Mechanized Proof of the Basic Perturbation Lemma.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Homological algebra, Basic perturbation lemma, Isabelle
1	Volker Haarslev, Ralf Möller	On the Scalability of Description Logic Instance Retrieval.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Instance retrieval, Description logics
1	Amine Chaieb, Tobias Nipkow	Proof Synthesis and Reflection for Linear Arithmetic.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Proof synthesis, Linear arithmetic, Reflection
1	Xavier Leroy, Sandrine Blazy	Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	The Coq proof assistant, Compilation, C, Program verification, Memory model, Compiler correctness
1	Magdalena Ortiz, Diego Calvanese, Thomas Eiter	Data Complexity of Query Answering in Expressive Description Logics via Tableaux.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Expressive description logics, Query answering, Data complexity
1	André Platzer	Differential Dynamic Logic for Hybrid Systems.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Verification of hybrid systems, Differential equations, Automated theorem proving, Dynamic logic, Sequent calculus, Axiomatisation
1	Yevgeny Kazakov, Boris Motik	A Resolution-Based Decision Procedure for SHOIQ.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Resolution decision procedures, Description logics, Nominals
1	Achim D. Brucker, Burkhart Wolff	An Extensible Encoding of Object-oriented Data Models in hol.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Verification, Theorem proving, Object-oriented data models, hol
1	Hasan Amjad	Data Compression for Proof Replay.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Proof translation, Interactive theorem proving, SAT solvers
1	Serge Autexier, Heiko Mantel, Stephan Merz, Tobias Nipkow	Preface.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF
1	Nick Moffat, Michael Goldsmith	Assumption-Commitment Support for CSP Model Checking.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Assumption-commitment, Model checking, Refinement, CSP, Compositional reasoning, Assume-guarantee
1	Osman Hasan, Sofiène Tahar	Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Coupon collector’s problem, HOL theorem prover, Probabilistic analysis, Higher-order-logic, Probability theory, Statistical properties
1	Roberto Gorrieri, Fabio Martinelli, Marinella Petrocchi	Formal Models and Analysis of Secure Multicast in Wired and Wireless Networks.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Formal security models and analysis, Multicast communication
1	Alastair F. Donaldson, Alice Miller	Automatic Symmetry Detection for Promela.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Model checking, Automatic verification, Promela, Symmetry reduction
1	Carsten Lutz, Maja Milicic	A Tableau Algorithm for Description Logics with Concrete Domains and General TBoxes.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	concrete domains, tableau algorithm, description logic, decidability
1	Swen Jacobs, Uwe Waldmann	Comparing Instance Generation Methods for Automated Reasoning.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	disconnection calculus, primal partial instantiation, resolution-based instance generation, theorem proving, automated reasoning
1	Roger Antonsen, Arild Waaler	Liberalized Variable Splitting.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	tableau calculus, variable splitting, first-order logic, free variables, connection method
1	Ruben Gamboa, John R. Cowles	Theory Extension in ACL2(r).	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	Mathematics Subject Classifications (2000) 68T15, 03B35, 03H15
1	Marc Aiguier, Diane Bahrami	Structures for Abstract Rewriting.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	abstract rewriting, abstract deduction procedure, abstract completion procedure, rewrite system, axiomatization
1	Neil V. Murray, Erik Rosenthal	Efficient Query Processing with Reduced Implicate Tries.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	reduced implicate trie, query processing, knowledge base
1	Martin Giese	Superposition-based Equality Handling for Analytic Tableaux.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	superposition rules, equality handling, analytic tableaux
1	Domenico Cantone, Marianna Nicolosi Asmundo	A Sound Framework for delta-Rule Variants in Free-Variable Semantic Tableaux.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	free-variable semantic tableaux, ?-rule, Skolemization
1	Thomas Raths, Jens Otten, Christoph Kreitz	The ILTP Problem Library for Intuitionistic Logic.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	ILTP, problem library, ATP, benchmarking, intuitionistic logic
1	Bernhard Beckert, Lawrence C. Paulson	Preface.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF
1	Jeremy Avigad, Kevin Donnelly	A Decision Procedure for Linear "Big O" Equations.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	Asymptotic equations, Big O, Decision procedures
1	Reinhold Letz, Gernot Stenz	The Disconnection Tableau Calculus.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	disconnection tableaux, theorem proving
1	Dominique Larchey-Wendling	Graph-based Decision for Gödel-Dummett Logics.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	Gödel-Dummett logic, countermodels, graphs, decision procedures, sequent calculus
1	Davide Bresolin, Angelo Montanari, Guido Sciavicco	An Optimal Decision Procedure for Right Propositional Neighborhood Logic.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	tableaux-based decision procedures, right propositional neighborhood logic, interval temporal logic
1	Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli	User Interaction with the Matita Proof Assistant.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	Mathematical knowledge management, XML, Digital libraries, Authoring, Interactive theorem proving, Proof assistant
1	David Aspinall, Christoph Lüth	Special Issue on User Interfaces in Theorem Proving: Preface.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF
1	Julien Narboux	A Graphical User Interface for Formal Proofs in Geometry.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	Interface, Geometry, Automated theorem proving, Theorem prover, Proof assistant, Coq, Dynamic geometry
1	Hans Kleine Büning, K. Subramani, Xishun Zhao	Boolean Functions as Models for Quantified Boolean Formulas.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	Model, Complexity, Boolean function, Satisfiability, Propositional logic, Quantified Boolean formula
1	Alberto Ciaffaglione, Luigi Liquori, Marino Miculan	Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	Functional and imperative object-calculi, Logical foundations of programming, Coinductive type theories, Logical frameworks, Interactive theorem proving
1	Ullrich Hustadt, Boris Motik, Ulrike Sattler	Reasoning in Description Logics by a Reduction to Disjunctive Datalog.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	Description logics, Data complexity, Disjunctive datalog
1	Stefan Schlobach, Zhisheng Huang, Ronald Cornet, Frank van Harmelen	Debugging Incoherent Terminologies.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	Debugging, Diagnosis, Description logics
1	Ian Horrocks, Ulrike Sattler	A Tableau Decision Procedure for SHOIQ.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	Description logic, Decision procedures
1	Carsten Sinz	Visualizing SAT Instances and Runs of the DPLL Algorithm.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	SAT instance, DPLL procedure
1	Barbara Morawska	General E -unification with Eager Variable Elimination and a Nice Cycle Rule.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	E-unification, Variable elimination, Cycle rule
1	William Billingsley, Peter Robinson	Student Proof Exercises Using MathsTiles and Isabelle/HOL in an Intelligent Book.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	Intelligent book, MathsTiles, Isabelle
1	Diego Calvanese, Giuseppe De Giacomo, Domenico Lembo, Maurizio Lenzerini, Riccardo Rosati	Tractable Reasoning and Efficient Query Answering in Description Logics: The DL-Lite Family.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	DL-Lite, Description logics, Query answering, Ontology languages
1	Dmitry Tsarkov, Ian Horrocks, Peter F. Patel-Schneider	Optimizing Terminological Reasoning for Expressive Description Logics.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	Reasoning systems, Optimizations, Description logic
1	Franz Baader	Preface to Special Issue on Reasoning in Description Logics.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF
1	Paul A. Cairns, Jeremy Gow	Integrating Searching and Authoring in Mizar.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	Alcor, Mizar, Information retrieval, LSI, Mathematics
1	Gem Stapleton, Judith Masthoff, Jean Flower, Andrew Fish, Jane Southern	Automated Theorem Proving in Euler Diagram Systems.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	Heuristics, Visual languages, Diagrammatic reasoning, Euler diagrams
1	Julien Forest, Delia Kesner	Expression Reduction Systems with Patterns.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	Expression reduction systems, Higher-order rewriting, Pattern matching
1	Daniel R. Brooks, Esra Erdem, Selim T. Erdogan, James W. Minett, Donald Ringe	Inferring Phylogenetic Trees Using Answer Set Programming.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	Cladistics, Answer set programming, Phylogeny
1	Bernd Fischer, Geoff Sutcliffe, Stephan Schulz	Empirically Successful Automated Reasoning: Applications Issue.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF
1	Josef Urban	MPTP 0.2: Design, Implementation, and Initial Experiments.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF	MPTP, Mizar, ATP, MPA, re-proving, proof discovery, MML
1	Carsten Sinz, Wolfgang Küchlin, Dieter Feichtinger, Georg Görtler	Checking Consistency and Completeness of On-Line Product Manuals.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF	problem encoding, BDD-techniques, SAT, real-world applications
1	Panagiotis Manolios, Sudarshan K. Srinivasan	A Framework for Verifying Bit-Level Pipelined Machines Based on Automated Deduction and Decision Procedures.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF	pipelined machines, bit-level, verification, refinement, automated reasoning, ACL2
1	Oliver Pell	Verification of FPGA Layout Generators in Higher-Order Logic.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF	layout description, circuit verification, FPGA, theorem proving
1	Gilles Audemard, Belaid Benhamou, Laurent Henocque	Predicting and Detecting Symmetries in FOL Finite Model Search.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF	symmetry, constraint programming, finite models
1	Carlos Simpson	Explaining Gabriel-Zisman Localization to the Computer.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF	calculus of fractions, computer proof verification, localization, category, proof assistant, functor
1	Alessandro Armando, David A. Basin, Jorge Cuéllar, Michaël Rusinowitch, Luca Viganò	Automated Reasoning for Security Protocol Analysis.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF
1	Andrew Ireland, Bill J. Ellis, Andrew Cook, Roderick Chapman, Janet Barnes	An Integrated Approach to High Integrity Software Verification.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF	static analysis, SPARK, proof planning, program proof
1	Graham Steel, Alan Bundy	Attacking Group Protocols by Refuting Incorrect Inductive Conjectures.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF	cryptographic security protocols, counterexamples, superposition
1	Bernd Löchner	Things to Know when Implementing KBO.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF	Knuth-Bendix ordering, program transformation
1	Keiichirou Kusakari, Masaki Nakamura, Yoshihito Toyama	Elimination Transformations for Associative-Commutative Rewriting Systems.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF	(AC-)termination, (AC-)dependency pair, argument filtering, elimination transformation
1	Stéphanie Delaune, Florent Jacquemard	Decision Procedures for the Security of Protocols with Probabilistic Encryption against Offline Dictionary Attacks.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF	verification, formal methods, cryptographic protocols, dictionary attacks, probabilistic encryption
1	Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard	Deciding Boolean Algebra with Presburger Arithmetic.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF	complexity, program verification, decision procedure, Boolean algebra, quantifier elimination, Presburger arithmetic
1	Rohit Chadha, Steve Kremer, Andre Scedrov	Formal Analysis of Multiparty Contract Signing.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF	multiparty contract signing, GM protocol
1	Enrico Giunchiglia, Yuliya Lierler, Marco Maratea	Answer Set Programming Based on Propositional Satisfiability.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF	answer set programming, propositional satisfiability
1	Hans Hüttel, Jirí Srba	Decidability Issues for Extended Ping-Pong Protocols.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF	replication, cryptographic protocols, formal modelling, recursion
1	Bernd Fischer, Geoff Sutcliffe, Stephan Schulz	Empirically Successful Automated Reasoning: Systems Issue.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF
1	Nick C. Fiala, Keith M. Agre	Searching for Shortest Single Axioms for Groups of Exponent 6.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF	exponent, single axiom, group, automated theorem-proving
1	Michael Beeson	Mathematical Induction in Otter-Lambda.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF	computer proofs, second-order, Otter, mathematical induction, unification, automated deduction

Publications at "J. Autom. Reasoning"( http://dblp.L3S.de/Venues/J._Autom._Reasoning )