Search results for "IJCAR"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
1	Geoff Sutcliffe	CASC-J4 The 4th IJCAR ATP System Competition.	IJCAR	2008	DBLP DOI BibTeX RDF
1	Adel Bouhoula, Florent Jacquemard	Automated Induction with Constrained Tree Automata.	IJCAR	2008	DBLP DOI BibTeX RDF
1	André Platzer, Jan-David Quesel	KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description).	IJCAR	2008	DBLP DOI BibTeX RDF	verification of hybrid systems, decision procedures, computer algebra, automated theorem proving, dynamic logic
1	Boris Motik, Ian Horrocks 0001	Individual Reuse in Description Logic Reasoning.	IJCAR	2008	DBLP DOI BibTeX RDF
1	Gilles Barthe, Benjamin Grégoire, Mariela Pavlova	Preservation of Proof Obligations from Java to the Java Virtual Machine.	IJCAR	2008	DBLP DOI BibTeX RDF
1	Andrey Paskevich	Connection Tableaux with Lazy Paramodulation.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Maria Paola Bonacina, Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli	Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Predrag Janicic, Pedro Quaresma	System Description: GCLCprover + GeoThms.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Jörg Endrullis, Johannes Waldmann, Hans Zantema	Matrix Interpretations for Proving Termination of Term Rewriting.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Shuvendu K. Lahiri, Madanlal Musuvathi	Solving Sparse Linear Constraints.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Franz Baader, Carsten Lutz, Boontawee Suntisrivaraporn	CEL - A Polynomial-Time Reasoner for Life Science Ontologies.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Yevgeny Kazakov, Boris Motik	A Resolution-Based Decision Procedure for SHOIQ.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Roy Dyckhoff, Delia Kesner, Stéphane Lengrand	Strong Cut-Elimination Systems for Hudelmaier's Depth-Bounded Sequent Calculus for Implicational Logic.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Jürgen Zimmer, Serge Autexier	The MathServe System for Semantic Web Reasoning Services.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Kaustuv Chaudhuri, Frank Pfenning, Greg Price	A Logical Characterization of Forward and Backward Chaining in the Inverse Method.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Florian Rabe 0001	First-Order Logic with Dependent Types.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Christoph Benzmüller, Chad E. Brown, Michael Kohlhase	Cut-Simulation in Impredicative Logics.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Sean McLaughlin	An Interpretation of Isabelle/HOL in HOL Light.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Chad E. Brown	Combining Type Theory and Untyped Set Theory.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Sylvie Boldo	Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Benjamin Grégoire, Laurent Théry	A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Olga Grinchtein, Martin Leucker, Nir Piterman	Inferring Network Invariants Automatically.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Bernhard Beckert, André Platzer	Dynamic Logic with Non-rigid Functions.	IJCAR	2006	DBLP DOI BibTeX RDF	logical foundations of programming languages, object-orientation, software verification, Dynamic logic, sequent calculus, program logic
1	Xiangxue Jia, Jian Zhang 0001	A Powerful Technique to Eliminate Isomorphism in Finite Model Search.	IJCAR	2006	DBLP DOI BibTeX RDF	LNH, DASH, scheme, Isomorphism, symmetry breaking
1	Geoff Sutcliffe	CASC-J3 - The 3rd IJCAR ATP System Competition.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Erik Reeber, Warren A. Hunt Jr.	A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA).	IJCAR	2006	DBLP DOI BibTeX RDF
1	Alexander Krauss 0001	Partial Recursive Functions in Higher-Order Logic.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Christian Urban, Stefan Berghofer	A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL.	IJCAR	2006	DBLP DOI BibTeX RDF	Lambda-calculus, proof assistants, nominal logic, primitive recursion
1	Joe Hendrix, José Meseguer 0001, Hitoshi Ohsaki	A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Anna Zamansky, Arnon Avron	Canonical Gentzen-Type Calculi with (n, k)-ary Quantifiers.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Dexter Kozen, Christoph Kreitz, Eva Richter	Automating Proofs in Category Theory.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Amine Chaieb	Verifying Mixed Real-Integer Quantifier Elimination.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi	Specifying and Reasoning About Dynamic Access-Control Policies.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Steven Obua, Sebastian Skalberg	Importing HOL into Isabelle/HOL.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Allen Van Gelder, Geoff Sutcliffe	Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation.	IJCAR	2006	DBLP DOI BibTeX RDF
1	David Toman 0001, Grant E. Weddell	On Keys and Functional Dependencies as First-Class Citizens in Description Logics.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Jordi Levy, Manfred Schmidt-Schauß, Mateu Villaret	Stratified Context Unification Is NP-Complete.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Assia Mahboubi	Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Hans de Nivelle, Jia Meng	Geometric Resolution: A Proof Procedure Based on Finite Model Search.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Dale Miller 0001	Representing and Reasoning with Operational Semantics.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Stéphane Demri, Denis Lugiez	Presburger Modal Logic Is PSPACE-Complete.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Roland Zumkeller	Formal Global Optimisation with Taylor Models.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Daria Walukiewicz-Chrzaszcz, Jacek Chrzaszcz	Consistency and Completeness of Rewriting in the Calculus of Constructions.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Peter Baumgartner 0001, Renate A. Schmidt	Blocking and Other Enhancements for Bottom-Up Model Generation Methods.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Robert L. Constable, Wojciech Moczydlowski	Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Volker Sorge, Andreas Meier 0002, Roy L. McCasland, Simon Colton	Automatic Construction and Verification of Isotopy Invariants.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Dmitry Tsarkov, Ian Horrocks 0001	FaCT++ Description Logic Reasoner: System Description.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Adam Koprowski, Hans Zantema	Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems.	IJCAR	2006	DBLP DOI BibTeX RDF
1	John Harrison 0001	Towards Self-verification of HOL Light.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Ulrich Furbach, Natarajan Shankar (eds.)	Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings	IJCAR	2006	DBLP DOI BibTeX RDF
1	Bruno Buchberger	Mathematical Theory Exploration.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Benjamin Werner	On the Strength of Proof-Irrelevant Type Theories.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Jürgen Giesl, Peter Schneider-Kamp, René Thiemann	Automatic Termination Proofs in the Dependency Pair Framework.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Brigitte Pientka	Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Florent Jacquemard, Michaël Rusinowitch, Laurent Vigneron	Tree Automata with Equality Constraints Modulo Equational Theories.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Geoff Sutcliffe, Stephan Schulz 0001, Koen Claessen, Allen Van Gelder	Using the TPTP Language for Writing Derivations and Finite Interpretations.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Tobias Nipkow, Gertrud Bauer, Paula Schultz	Flyspeck I: Tame Graphs.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Viorica Sofronie-Stokkermans	Interpolation in Local Theory Extensions.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Adnan Darwiche	Searching While Keeping a Trace: The Evolution from Satisfiability to Knowledge Compilation.	IJCAR	2006	DBLP DOI BibTeX RDF
1	Yevgeny Kazakov, Hans de Nivelle	A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards.	IJCAR	2004	DBLP DOI BibTeX RDF
1	David A. Basin, Michaël Rusinowitch (eds.)	Automated Reasoning - Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings	IJCAR	2004	DBLP DOI BibTeX RDF
1	Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar	The ICS Decision Procedures for Embedded Deduction.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Ewen Denney, Bernd Fischer 0002, Johann Schumann	Using Automated Theorem Provers to Certify Auto-generated Aerospace Software.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Guillem Godoy, Ashish Tiwari 0001	Deciding Fundamental Properties of Right-(Ground or Variable) Rewrite Systems by Rewrite Closure.	IJCAR	2004	DBLP DOI BibTeX RDF
1	René Thiemann, Jürgen Giesl, Peter Schneider-Kamp	Improved Modular Termination Proofs Using Dependency Pairs.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Ullrich Hustadt, Boris Konev, Alexandre Riazanov, Andrei Voronkov	TeMP: A Temporal Monodic Prover.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Anni-Yasmin Turhan, Christian Kissig	Sonic - Non-standard Inferences Go OilEd.	IJCAR	2004	DBLP DOI BibTeX RDF
1	K. Subramani 0001	Analyzing Selected Quantified Integer Programs.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Michael Beeson	Lambda Logic.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Stephan Schulz 0001	System Description: E 0.81.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Miquel Bofill, Albert Rubio	Redundancy Notions for Paramodulation with Non-monotonic Orderings.	IJCAR	2004	DBLP DOI BibTeX RDF
1	José Meseguer 0001, Grigore Rosu	Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Bernd Löchner	A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Filip Maric, Predrag Janicic	argo-lib: A Generic Platform for Decision Procedures.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Dominique Larchey-Wendling	Counter-Model Search in Gödel-Dummett Logics.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Tanel Tammet	Chain Resolution for the Semantic Web.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Thierry Boy de la Tour, Mnacho Echenim	Overlapping Leaf Permutative Equations.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Reinhold Letz, Gernot Stenz	Generalised Handling of Variables in Disconnection Tableaux.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Simon Colton, Andreas Meier 0002, Volker Sorge, Roy L. McCasland	Automatic Generation of Classification Theorems for Finite Algebras.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Geoff Sutcliffe, Christian B. Suttner	The CADE ATP System Competition.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Jeremy Avigad, Kevin Donnelly	Formalizing O Notation in Isabelle/HOL.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Volker Weispfenning	Solving Constraints by Elimination Methods.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Ting Zhang 0001, Henny B. Sipma, Zohar Manna	Decision Procedures for Recursive Data Structures with Integer Constraints.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Jia Meng, Lawrence C. Paulson	Experiments on Supporting Interactive Proof Using Resolution.	IJCAR	2004	DBLP DOI BibTeX RDF
1	William M. Farmer	Formalizing Undefinedness Arising in Calculus.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Graham Steel, Alan Bundy, Monika Maidl	Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Franz Baader, Silvio Ghilardi, Cesare Tinelli	A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Daniel Winterstein, Alan Bundy, Corin A. Gurr	Dr.Doodle: A Diagrammatic Theorem Prover.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Alexandre Riazanov, Andrei Voronkov	Efficient Checking of Term Ordering Constraints.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Jürgen Avenhaus	Efficient Algorithms for Computing Modulo Permutation Theories.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Carsten Lutz, Dirk Walther 0002	PDL with Negation of Atomic Programs.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann	Modular Proof Systems for Partial Functions with Weak Equality.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Gilles Barthe, Jan Cederquist, Sabrina Tarento	A Machine-Checked Formalization of the Generic Model and the Random Oracle Model.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Georg Gottlob	Second-Order Logic over Finite Structures - Report on a Research Programme.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Richard Bonichon	TaMeD: A Tableau Method for Deduction Modulo.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Àngel J. Gil, Miki Hermann, Gernot Salzer, Bruno Zanuttini	Efficient Algorithms for Constraint Description Problems over Finite Totally Ordered Domains: Extended Abstract.	IJCAR	2004	DBLP DOI BibTeX RDF
1	Jürgen Stuber	A Model-Based Completeness Proof of Extended Narrowing and Resolution.	IJCAR	2001	DBLP DOI BibTeX RDF
1	Jürgen Avenhaus, Bernd Löchner	CCE: Testing Ground Joinability.	IJCAR	2001	DBLP DOI BibTeX RDF
1	Alexandre Riazanov, Andrei Voronkov	Vampire 1.1 (System Description).	IJCAR	2001	DBLP DOI BibTeX RDF
1	Reiner Hähnle, Neil V. Murray, Erik Rosenthal	Ordered Resolution vs. Connection Graph Resolution.	IJCAR	2001	DBLP DOI BibTeX RDF

Publications at "IJCAR"( http://dblp.L3S.de/Venues/IJCAR )