VLDB 2026 Research / reviewers in the wild / expert
Michael Kifer
dblp:k/MichaelKifer
· DBLP profile ↗
60ranked-venue papers
18as first author
2since 2021 · last 2024
0000-0003-3177-5792ORCID · verified
Domains — the database's venue-derived domains; a paper can count in several
Databases, data management, data science and information retrieval · 27 · 9 first-authorArtificial intelligence and machine learning · 14 · 3 first-author · 1 since 2021Theory of computation · 14 · 5 first-author · 1 since 2021Software engineering, systems software and programming languages · 13 · 1 first-author · 1 since 2021Applied, interdisciplinary, general and emerging computing · 5 · 2 first-authorGraphics, computer vision, multimedia, augmented reality and games · 3Human-computer interaction and ubiquitous computing · 1
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2024 | Multi-paradigm Logic Programming in the ErgoAI System
Theresa Swift, Michael Kifer |
LPNMR | 2 |
| 2023 | Knowledge Authoring for Rules and ActionsabstractAbstract Knowledge representation and reasoning (KRR) systems describe and reason with complex concepts and relations in the form of facts and rules. Unfortunately, wide deployment of KRR systems runs into the problem that domain experts have great difficulty constructing correct logical representations of their domain knowledge. Knowledge engineers can help with this construction process, but there is a deficit of such specialists. The earlier Knowledge Authoring Logic Machine (KALM) based on Controlled Natural Language (CNL) was shown to have very high accuracy for authoring facts and questions. More recently, KALMFL, a successor of KALM, replaced CNL with factual English, which is much less restrictive and requires very little training from users. However, KALMFL has limitations in representing certain types of knowledge, such as authoring rules for multi-step reasoning or understanding actions with timestamps. To address these limitations, we propose KALMRA to enable authoring of rules and actions. Our evaluation using the UTI guidelines benchmark shows that KALMRA achieves a high level of correctness (100%) on rule authoring. When used for authoring and reasoning with actions, KALMRA achieves more than 99.3% correctness on the bAbI benchmark, demonstrating its effectiveness in more sophisticated KRR jobs. Finally, we illustrate the logical reasoning capabilities of KALMRA by drawing attention to the problems faced by the recently made famous AI, ChatGPT. Paul Fodor, Michael Kifer |
Theory Pract. Log. Program. | 3 |
| 2019 | Querying Knowledge via Multi-Hop English QuestionsabstractAbstract The inherent difficulty of knowledge specification and the lack of trained specialists are some of the key obstacles on the way to making intelligent systems based on the knowledge representation and reasoning (KRR) paradigm commonplace.Knowledge and query authoringusing natural language, especiallycontrollednatural language (CNL), is one of the promising approaches that could enable domain experts, who are not trained logicians, to both create formal knowledge and query it. In previous work, we introduced theKALMsystem (Knowledge Authoring Logic Machine) that supports knowledge authoring (and simple querying) with very high accuracy that at present is unachievable via machine learning approaches. The present paper expands on the question answering aspect of KALM and introducesKALM-QA(KALM for Question Answering) that is capable of answering much more complex English questions. We show that KALM-QA achieves 100% accuracy on an extensive suite of movie-related questions, calledMetaQA, which contains almost 29,000 test questions and over 260,000 training questions. We contrast this with a published machine learning approach, which falls far short of this high mark. Tiantian Gao, Paul Fodor, Michael Kifer |
Theory Pract. Log. Program. | 3 |
| 2018 | Formal Executable Theory of Multilevel Modeling
Mira Balaban, Igal Khitron, Michael Kifer, Azzam Maraee |
CAiSE | 3 |
| 2018 | High Accuracy Question Answering via Hybrid Controlled Natural LanguageabstractKnowledge representation and reasoning (KRR) is key to the vision of the intelligent Web. Unfortunately, wide deployment of KRR is hindered by the difficulty in specifying the requisite knowledge, which requires skills that most domain experts lack. A way around this problem could be to acquire knowledge automatically from documents. The difficulty is that, KRR requires high-precision knowledge and is sensitive even to small amounts of errors. Although most automatic information extraction systems developed for general text understandings have achieved remarkable results, their accuracy is still woefully inadequate for logical reasoning. A promising alternative is to ask the domain experts to author knowledge in Controlled Natural Language (CNL). Nonetheless, the quality of knowledge construction even through CNL is still grossly inadequate, the main obstacle being the multiplicity of ways the same information can be described even in a controlled language. Our previous work addressed the problem of high accuracy knowledge authoring for KRR from CNL documents by introducing the Knowledge Authoring Logic Machine (KALM). This paper develops the query aspect of KALM with the aim of getting high precision answers to CNL questions against previously authored knowledge and is tolerant to linguistic variations in the queries. To make queries more expressive and easier to formulate, we propose a hybrid CNL, i.e., a CNL with elements borrowed from formal query languages. We show that KALM achieves superior accuracy in semantic parsing of such queries. Tiantian Gao, Paul Fodor, Michael Kifer |
WI | 3 |
| 2016 | Formalizing Goal Serializability for Evaluation of Planning Features
Reza Basseda, Michael Kifer |
JELIA | 2 |
| 2016 | Paraconsistency and word puzzlesabstractAbstract Word puzzles and the problem of their representations in logic languages have received considerable attention in the last decade (Ponnuruet al. 2004; Shapiro 2011; Baral and Dzifcak 2012; Schwitter 2013). Of special interest is the problem of generating such representations directly from natural language (NL) or controlled natural language (CNL). An interesting variation of this problem, and to the best of our knowledge, scarcely explored variation in this context, is when the input information is inconsistent. In such situations, the existing encodings of word puzzles produce inconsistent representations and break down. In this paper, we bring the well-known type of paraconsistent logics, calledAnnotated Predicate Calculus(APC) (Kifer and Lozinskii 1992), to bear on the problem. We introduce a new kind of non-monotonic semantics for APC, calledconsistency preferred stable modelsand argue that it makes APC into a suitable platform for dealing with inconsistency in word puzzles and, more generally, in NL sentences. We also devise a number of general principles to help the user choose among the different representations of NL sentences, which might seem equivalent but, in fact, behave differently when inconsistent information is taken into account. These principles can be incorporated into existing CNL translators, such as Attempto Controlled English (ACE) (Fuchset al. 2008) and PENG Light (White and Schwitter 2009). Finally, we show that APC with the consistency preferred stable model semantics can be equivalently embedded in ASP with preferences over stable models, and we use this embedding to implement this version of APC in Clingo (Gebseret al. 2011) and its Asprin add-on (Brewkaet al. 2015). Tiantian Gao, Paul Fodor, Michael Kifer |
Theory Pract. Log. Program. | 3 |
| 2015 | State Space Planning Using Transaction Logic
Reza Basseda, Michael Kifer |
PADL | 2 |
| 2013 | Terminyzer: An Automatic Non-termination Analyzer for Large Logic Programs
Senlin Liang, Michael Kifer |
PADL | 2 |
| 2013 | Taming the Infinite Chase: Query Answering under Expressive Relational ConstraintsabstractThe chase algorithm is a fundamental tool for query evaluation and for testing query containment under tuple-generating dependencies (TGDs) and equality-generating dependencies (EGDs). So far, most of the research on this topic has focused on cases where the chase procedure terminates. This paper introduces expressive classes of TGDs defined via syntactic restrictions: guarded TGDs (GTGDs) and weakly guarded sets of TGDs (WGTGDs). For these classes, the chase procedure is not guaranteed to terminate and thus may have an infinite outcome. Nevertheless, we prove that the problems of conjunctive-query answering and query containment under such TGDs are decidable. We provide decision procedures and tight complexity bounds for these problems. Then we show how EGDs can be incorporated into our results by providing conditions under which EGDs do not harmfully interact with TGDs and do not affect the decidability and complexity of query answering. We show applications of the aforesaid classes of constraints to the problem of answering conjunctive queries in F-Logic Lite, an object-oriented ontology language, and in some tractable Description Logics. Andrea Calì, Georg Gottlob, Michael Kifer |
J. Artif. Intell. Res. | 3 |
| 2013 | A practical analysis of non-termination in large logic programsabstractAbstract A large body of work has been dedicated to termination analysis of logic programs but relatively little has been done to analyze non-termination. In our opinion, explaining non-termination is a much more important task because it can dramatically improve a user's ability to effectively debug large, complex logic programs without having to abide by punishing syntactic restrictions. Non-termination analysis examines program execution history when the program is suspected to not terminate and informs the programmer about the exact reasons for this behavior. In Liang and Kifer (2013), we studied the problem of non-termination in tabled logic engines with subgoal abstraction, such as XSB, and proposed a suite of algorithms for non-termination analysis, called Terminyzer. These algorithms analyze forest logging traces and output sequences of tabled subgoal calls that are the likely causes of non-terminating cycles. However, this feedback was hard to use in practice: the same subgoal could occur in multiple rule heads and in even more places in rule bodies, so Terminyzer left too much tedious, sometimes combinatorially large amount of work for the user to do manually. Here we propose a new suite of algorithms, Terminyzer+, which closes this usability gap. Terminyzer+ can detect not only sequences of subgoals that cause non-termination, but, importantly, the exact rules where they occur and the rule sequences that get fired in a cyclic manner, thus causing non-termination. This makes Terminyzer+ suitable as a back-end for user-friendly graphical interfaces on top of Terminyzer+, which can greatly simplify the debugging process. Terminyzer+ back-ends exist for the SILK system as well as for the open-source ${\cal F}$ lora-2 system. A graphical interface has been developed for SILK and is currently underway for ${\cal F}$ lora-2. We also report experimental studies, which confirm the effectiveness of Terminyzer+ on a host of large real-world knowledge bases. All tests used in this paper are available online.1 In addition, we make a step towards automatic remediation of non-terminating programs by proposing an algorithm that heuristically fixes some causes of misbehavior. Furthermore, unlike Terminyzer, Terminyzer+ does not require the underlying logic engine to support subgoal abstraction, although it can make use of it. Senlin Liang, Michael Kifer |
Theory Pract. Log. Program. | 2 |
| 2011 | Logic-Based Model-Level Software Development with F-OML
Mira Balaban, Michael Kifer |
MoDELS | 2 |
| 2010 | Ontological Reasoning with F-logic Lite and its ExtensionsabstractAnswering queries posed over knowledge bases is a central problem in knowledge representation and database theory. In the database area, checking query containment is an important query optimization and schema integration technique. In knowledge representation it has been used for object classification, schema integration, service discovery, and more. In the presence of a knowledge base, the problem of query containment is strictly related to that of query answering; indeed, the two are reducible to each other; we focus on the latter, and our results immediately extend to the former. Andrea Calì, Georg Gottlob, Michael Kifer, Thomas Lukasiewicz, Andreas Pieris |
AAAI | 3 |
| 2010 | Rule Interchange Format: Logic Programming's Second Wind?
Michael Kifer |
ILP | 1 |
| 2010 | Tabling for transaction logicabstractTransaction Logic is a logic for representing declarative and procedural knowledge in logic programming, databases, and AI. It has been successful in areas as diverse as workflows and Web services, security policies, AI planning, reasoning about actions, and more. Although a number of implementations of Transaction Logic exist, none is logically complete due to the inherent difficulty and time/space complexity of such implementations. In this paper we attack this problem by first introducing a logically complete tabling evaluation strategy for Transaction Logic and then describing a series of optimizations, which make this algorithm practical. In support of our arguments, we present a performance evaluation study of six different implementations of this algorithm, each successively adopting our optimizations. The study suggest that the tabling algorithm can scale well both in time and space. We also discuss ideas that could improve the performance further. Paul Fodor, Michael Kifer |
PPDP | 2 |
| 2010 | Deriving predicate statistics in datalogabstractDatabase query optimizers rely on data statistics in selecting query execution plans. Similar query optimization techniques are desirable for deductive databases and, to make this happen, we need to be able to collect data statistics for Datalog predicates. The difficulty is, however, that Datalog predicates can be recursive. In this paper, we propose an algorithm, called SDP, that estimates Datalog query sizes efficiently by maintaining the statistical dependency information for derived predicates. Base predicate statistics are computed and summarized using dependency matrices, and derived predicate statistics are computed by evaluating rules in an abstract way with rule bodies replaced with algebraic expressions over the dependency matrices. Recursive rules are handled by a fixed point evaluation. Our experimental study validates that: 1) SDP produces better query size estimates than using base predicate statistics and propagating them to derived predicates using the argument independence assumption; 2) the estimates largely preserve the relative order of real query sizes and thus can be used to guide cost based query optimizers. Senlin Liang, Michael Kifer |
PPDP | 2 |
| 2010 | A Guide to the Basic Logic Dialect for Rule Interchange on the WebabstractThe W3C Rule Interchange Format (RIF) is a forthcoming standard for exchanging rules among different systems and developing intelligent rule-based applications for the Semantic Web. The RIF architecture is conceived as a family of languages, called dialects. A RIF dialect is a rule-based language with an XML syntax and a well-defined semantics. The RIF Basic Logic Dialect (RIF-BLD) semantically corresponds to a Horn rule language with equality. RIF-BLD has a number of syntactic extensions with respect to traditional textbook Horn logic, which include F-logic frames and predicates with named arguments. RIF-BLD is also well integrated with the relevant Web standards. It provides Internationalized Resource Identifiers (IRIs), XML Schema datatypes, and is aligned with RDF and OWL. This paper is a guide to the essentials of RIF-BLD, its syntax, semantics, and XML serialization. At the same time, some important RIF-BLD features are omitted due to the space limitations, including datatypes, built-ins, and the integration with RDF and OWL. Harold Boley, Michael Kifer |
IEEE Trans. Knowl. Data Eng. | 2 |
| 2009 | Logic Programming with Defaults and Argumentation Theories
Hui Wan 0001, Benjamin N. Grosof, Michael Kifer, Paul Fodor, Senlin Liang |
ICLP | 3 |
| 2009 | Belief Logic Programming: Uncertainty Reasoning with Correlation of Evidence
Hui Wan 0001, Michael Kifer |
LPNMR | 2 |
| 2009 | OpenRuleBench: an analysis of the performance of rule enginesabstractThe Semantic Web initiative has led to an upsurge of the interest in rules as a general and powerful way of processing, combining, and analyzing semantic information. Since several of the technologies underlying rule-based systems are already quite mature, it is important to understand how such systems might perform on the Web scale. OpenRuleBench is a suite of benchmarks for analyzing the performance and scalability of different rule engines. Currently the study spans five different technologies and eleven systems, but OpenRuleBench is an open community resource, and contributions from the community are welcome. In this paper, we describe the tested systems and technologies, the methodology used in testing, and analyze the results. Senlin Liang, Paul Fodor, Hui Wan 0001, Michael Kifer |
WWW | 4 |
| 2008 | WSMO Choreography: From Abstract State Machines to Concurrent Transaction Logic
Dumitru Roman, Michael Kifer, Dieter Fensel |
ESWC | 2 |
| 2008 | Taming the Infinite Chase: Query Answering under Expressive Relational Constraints
Andrea Calì, Georg Gottlob, Michael Kifer |
KR | 3 |
| 2008 | Semantic Web Service Choreography: Contracting and Enactment
Dumitru Roman, Michael Kifer |
ISWC | 2 |
| 2007 | Reasoning about the Behavior of Semantic Web Services with Concurrent Transaction Logic
Dumitru Roman, Michael Kifer |
VLDB | 2 |
| 2006 | Efficiently ordering subgoals with access constraintsabstractIn this paper, we study the problem of ordering subgoals under binding pattern restrictions for queries posed as nonrecursive Datalog programs. We prove that despite their limited expressive power, the problem is computationally hard — PSPACE-complete in the size of the nonrecursive Datalog program even for fairly restricted cases. As a practical solution to this problem, we develop an asymptotically optimal algorithm that runs in time linear in the size of the query plan. We also study extensions of our algorithm that efficiently solve other query planning problems under binding pattern restrictions. These problems include conjunctive queries with nested grouping constraints, distributed conjunctive queries, and first-order queries. Guizhen Yang, Michael Kifer, Vinay K. Chaudhri |
PODS | 2 |
| 2006 | Containment of Conjunctive Object Meta-Queries
Andrea Calì, Michael Kifer |
VLDB | 2 |
| 2005 | Nonmonotonic Reasoning in FLORA-2
Michael Kifer |
LPNMR | 1 |
| 2004 | Semantic bookmarking for non-visual web accessabstractBookmarks are shortcuts that enable quick access of the desired Web content. They have become a standard feature in any browser and recent studies have shown that they can be very useful for non-visual Web access as well. Current bookmarking techniques in assistive Web browsers are rigidly tied to the structure of Web pages. Consequently they are susceptible to even slight changes in the structure of Web pages. In this paper we propose semantic bookmarking for non-visual Web access. With the help of an ontology that represents concepts in a domain, content in Web pages can be semantically associated with bookmarks. As long as these associations can be identified, semantic bookmarks are resilient in the face of structural changes to the Web page. The use of ontologies allows semantic bookmarks to span multiple Web sites covered by a common domain. This contributes to the ease of information retrieval and bookmark maintenance. In this paper we describe highly automated techniques for creating and retrieving semantic bookmarks. These techniques have been incorporated into an assistive Web browser. Preliminary experimental evidence suggests the effectiveness of semantic bookmarks for non-visual Web access. Saikat Mukherjee, I. V. Ramakrishnan, Michael Kifer |
ASSETS | 3 |
| 2003 | On the complexity of schema inference from web pages in the presence of nullable data attributesabstractAn increasingly large number of Web pages are machine-generated by filling in templates with data stored in backend databases. These templates can be viewed as the implicit schemas of those Web pages. The ability to infer the implicit schema from a collection of Web pages is important for scalable data extraction, since the inferred schema can be used to automatically identify schema attributes that are "encoded" in Web pages.However, the task of inferring a "good" schema is complicated due to the existence of nullable (missing) data attributes. Usually if an attribute contains a null value, then it will be omitted in the generated Web page, giving rise to different variations and permutations of layout structures in Web pages that are generated from the same template.In this paper we investigate the complexity of schema inference from Web pages in the presence of nullable data attributes. We introduce the notion of unambiguity as a quality measure for inferred schemas and prove that the problem of inferring "good" (unambiguous) schemas is NP-complete. Our complexity results imply that ambiguity resolution is one of the root causes of the computational difficulty underlying schema inference from Web pages. Guizhen Yang, I. V. Ramakrishnan, Michael Kifer |
CIKM | 3 |
| 2002 | A Logical Framework for Scheduling Workflows under Resource Allocation Constraints
Pinar Karagöz, Michael Kifer, Ismail Hakki Toroslu |
VLDB | 2 |
| 2000 | Computational Aspects of Resilient Data Extraction from Semistructured SourcesabstractAutomatic data extraction from semistructured sources such as HTML pages is rapidly growing into a problem of significant importance, spurred by the growing popularity of the so called “shopbots” that enable end users to compare prices of goods and other services at various web sites without having to manually browse and fill out forms at each one of these sites. Hasan Davulcu, Guizhen Yang, Michael Kifer, I. V. Ramakrishnan |
PODS | 3 |
| 1999 | A Layered Architecture for Querying Dynamic Web ContentabstractThe design of webbases, database systems for supporting Web-based applications, is currently an active area of research. In this paper, we propose a 3-year architecture for designing and implementing webbases for querying dynamic Web content(i.e., data that can only be extracted by filling out multiple forms). The lowest layer, virtual physical layer, provides navigation independence by shielding the user from the complexities associated with retrieving data from raw Web sources. Next, the traditional logical layer supports site independence. The top layer is analogous to the external schema layer in traditional databases. Hasan Davulcu, Juliana Freire, Michael Kifer, I. V. Ramakrishnan |
SIGMOD Conference | 3 |
| 1998 | Logic Based Modeling and Analysis of WorkflowsabstractWC propose Concurrent Transaction Logic (C7X) as the language for specifying, analyzing, and scheduling of workflows.We show that both local and global properties of worktlows can be naturally represented as C7X formulas and reasoning can be done with the use of the proof theory and the semantics of this logic, We describe a transformation that leads to an eilicicnt algorithm for scheduling worldlows in the presencc of global temporal constraints, which leads to decision proccdurcs for dealing with several safety related properties such as whether every valid execution of the workflow satisfits a particular property or whether a worlcfiow execution is consistent with some given global constraints on the ordering of events in a workflow.We also provide tight complexity results on the running times of these algorithms. Hasan Davulcu, Michael Kifer, C. R. Ramakrishnan 0001, I. V. Ramakrishnan |
PODS | 2 |
| 1998 | On the Decidability and Axiomatization of Query Finiteness in Deductive DatabasesabstractA database query is finite if its result consists of a finite sets tuples. For queries formulated as sets of pure Horn rules, the problem of determining finiteness is, in general, undecidable. In this paper, we consider superfiniteness —a stronger kind of finiteness, which applies to Horn queries whose function symbols are replaced by the abstraction of infinite relations with finiteness constraints (abbr., FC's). We show that superfiniteness is not only decidable but also axiomatizable , and the axiomatization yields an effective decision procedure. Although there are finite queries that are not superfinite, we demonstrate that superfinite queries represent an interesting and nontrivial subclass within the class of all finite queries. The we turn to the issue of inference of finiteness constraints—an important practical problem that is instrumental in deciding if a query is evaluable by a bottom-up algorithm. Although it is not known whether FC-entailment is decidable for sets of function-free Horn rules, we show that super-entailment , a stronger form of entailment, is decidable. We also show how a decision procedure for super-entailment can be used to enhance tests for query finiteness. Michael Kifer |
J. ACM | 1 |
| 1995 | Sorted HiLog: Sorts in Higher-Order Logic Data Languages
Weidong Chen 0005, Michael Kifer |
ICDT | 2 |
| 1995 | Logical Foundations of Object-Oriented and Frame-Based LanguagesabstractWe propose a novel formalism, calledFrame Logic(abbr., F-logic), that accounts in a clean and declarative fashion for most of the structural aspects of object-oriented and frame-based languages. These features include object identity, complex objects, inheritance, polymorphic types, query methods, encapsulation, and others. In a sense, F-logic stands in the same relationship to the object-oriented paradigm as classical predicate calculus stands to relational programming. F-logic has a model-theoretic semantics and a sound and complete resolution-based proof theory. A small number of fundamental concepts that come from object-oriented programming have direct representation in F-logic; other, secondary aspects of this paradigm are easily modeled as well. The paper also discusses semantic issues pertaining to programming with a deductive object-oriented language based on a subset of F-logic. Michael Kifer, Georg Lausen, James Wu |
J. ACM | 1 |
| 1995 | Forword: Deductive Object-Oriented Databases
Michael Kifer |
J. Intell. Inf. Syst. | 1 |
| 1994 | An Overview of Transaction Logic
Anthony J. Bonner, Michael Kifer |
Theor. Comput. Sci. | 2 |
| 1993 | Transaction Logic Programming
Anthony J. Bonner, Michael Kifer |
ICLP | 2 |
| 1993 | A Theory of Nonmonotonic Inheritance Based on Annotated Logic
Krishnaprasad Thirunarayan, Michael Kifer |
Artif. Intell. | 2 |
| 1993 | A Logic Programming with Complex Objects
Michael Kifer, James Wu |
J. Comput. Syst. Sci. | 1 |
| 1992 | Querying Object-Oriented DatabasesabstractWe present a novel language for querying object-oriented databases. The language is built around the idea of extended path expressions that substantially generalize [ZAN83], and on an adaptation of the first-order formalization of object-oriented languages from [KW89, KLW90, KW92]. The language incorporates features not found in earlier proposals; it is easier to use and has greater expressive power. Some of the salient features of our language are: ffl Precise model-theoretic semantics. ffl A very expressive form of path expressions that not only can do joins, selections and unnesting, but can also be used to explore the database schema. ffl Views can be defined and manipulated in a much more uniform way than in other proposals. ffl Database schema can be explored in the very same language that is used to retrieve data. Unlike in relational languages, the user needs not know anything about the system tables that store schema information. ffl The notions of a type and type-correctness have precise meaning. It accommodates a wide variety of queries that might be deemed well- or ill-typed under different circumstances. In particular, we show that there is more than one way of settling the issue of type correctness. For expository purposes and due to space limitation, we chose to make a number of simplifying assumptions and left some features out. A more complete account can be found in [KSK92]. Michael Kifer, Won Kim 0001, Yehoshua Sagiv |
SIGMOD Conference | 1 |
| 1992 | A Logic for Reasoning with Inconsistency
Michael Kifer, Eliezer L. Lozinskii |
J. Autom. Reason. | 1 |
| 1991 | A First-Order Theory of Types and Polymorphism in Logic ProgrammingabstractA logic called typed predicate calculus (TPC) that gives declarative meaning to logic programs with type declarations and type inference is introduced. The proper interaction between parametric and inclusion varieties of polymorphism is achieved through a construct called type dependency, which is analogous to implication types but yields more natural and succinct specifications. Unlike other proposals where typing has extra-logical status, in TPC the notion of type-correctness has precise model-theoretic meaning that is independent of any specific type-checking or type-inference procedure. Moreover, many different approaches to typing that were proposed in the past can be studied and compared within the framework of TPC. Another novel feature of TPC is its reflexivity with respect to type declarations; in TPC, these declarations can be queried the same way as any other data. Type reflexivity is useful for browsing knowledge bases and, potentially, for debugging logic programs.> Michael Kifer, James Wu |
LICS | 1 |
| 1990 | On Compile-Time Query Optimization in Deductive Databases by Means of Static FilteringabstractWe extend the query optimization techniques known as algebric manipulations with relational expressions [48] to work with deductive databases. In particular, we propose a method for moving data-independent selections and projections into recursive axioms, which extends all other known techniques for performing that task [2, 3, 9, 18, 20]. We also show that, in a well-defined sense, our algorithm is optimal among the algorithms that propagate data-independent selections through recursion. Michael Kifer, Eliezer L. Lozinskii |
ACM Trans. Database Syst. | 1 |
| 1989 | An Evidence-based Framework for a Theory of Inheritance
Krishnaprasad Thirunarayan, Michael Kifer |
IJCAI | 2 |
| 1989 | On the Declarative Semantics of Inheritance Networks
Krishnaprasad Thirunarayan, Michael Kifer, David Scott Warren |
IJCAI | 2 |
| 1989 | RI: A Logic for Reasoning with InconsistencyabstractThe authors present a logic, called RI (reasoning with inconsistency), that treats any set of clauses, either consistent or not, in a uniform way. In this logic, consequences of a contradiction are not nearly as damaging as in the standard predicate calculus, and meaningful information can still be extracted from an inconsistent set of formulas. RI has a resolution-based sound and complete proof procedure. It is a much richer logic than the predicate calculus, and the latter can be imitated within RI in several different ways (depending on the intended meaning of the predicate calculus formulas). The authors also introduce a novel notion of epistemic entailment and show its importance for investigating inconsistency in the predicate calculus.> Michael Kifer, Eliezer L. Lozinskii |
LICS | 1 |
| 1989 | A Logic for Object-Oriented Logic Programming (Maier's O-Logic Revisited)abstractWe present a logic for reasoning about complex objects, which is a revised and significantly extended version of Maier's O-logic [Mai86]. The logic naturally supports complex objects, object identity, deduction, is tolerant to inconsistent data, and has many other interesting features. It elegantly combines the object-oriented and value-oriented paradigms and, in particular, contains all of the predicate calculus as a special case. Our treatment of sets is also noteworthy: it is more general than ELPS [Kup87] and COL [AbG87], yet it avoids the semantic problems encountered in LDL [BNS87]. The proposed logic has a sound and complete resolution-based proof procedure. Michael Kifer, James Wu |
PODS | 1 |
| 1989 | F-Logic: A Higher-Order language for Reasoning about Objects, Inheritance, and SchemeabstractWe propose a database logic which accounts in a clean declarative fashion for most of the “object-oriented” features such as object identity, complex objects, inheritance, methods, etc. Furthermore, database schema is part of the object language, which allows the user to browse schema and data using the same declarative formalism. The proposed logic has a formal semantics and a sound and complete resolution-based proof procedure, which makes it also computationally attractive. Michael Kifer, Georg Lausen |
SIGMOD Conference | 1 |
| 1988 | On the Semantics of Rule-Based Expert Systems with Uncertainty
Michael Kifer, Ai Li |
ICDT | 1 |
| 1988 | An Axiomatic Approach to Deciding Query Safety in Deductive DatabasesabstractA database query is safe if its result consists of a finite set of tuples. If a query is expressed using a set of pure Horn Clauses, the problem of determining query safety is, in general, undecidable. In this paper we consider a slightly stronger notion of safety, called supersafety, for Horn databases in which function symbols are replaced by the abstraction of infinite relations with finiteness constraints [Ramarkrishman et. al 87] We show that the supersafety problem is not only decidable, but also axiomatizable, and the axiomatization yields an effective decision procedure. Although there are safe queries which are not supersafe, we demonstrate that the latter represent quite a large and nontrivial portion of the safe of all safe queries Michael Kifer, Raghu Ramakrishnan 0001, Avi Silberschatz |
PODS | 1 |
| 1988 | SYGRAF: Implementing Logic Programs in a Database StyleabstractIt is shown how Horn logic programs can be implemented using database techniques, namely, mostly bottom-up in combination with certain top-down elements (as opposed to the top-down implementations of logic programs prevailing so far). The proposed method is sound and complete. It easily lends itself to a parallel implementation and is free of nonlogical features like backtracking. As an extension to the common approach to deductive databases, function symbols are allowed to appear in programs, and it is shown that much of database query optimization can be applied to optimize logic programs. An important advantage of present approach is its ability to evaluate successfully many programs that terminate under neither pure top-down nor bottom-up evaluation strategies.> Michael Kifer, Eliezer L. Lozinskii |
IEEE Trans. Software Eng. | 1 |
| 1987 | Implementing Logic Programs as a Database SystemabstractWe show how Horn logic programs can be implemented using database techniques, namely, mostly bottom-up in combination with certain top-down elements (as opposed to the top-down implementations of logic programs prevailing so far). The proposed method is sound and complete. It easily lends itself to a parallel implementation, and is free of nonlogical features, like backtracking. In extension to the common approach to deductive databases, we allow function symbols to appear in programs. An important advantage of this method is that it terminates in many cases in which PROLOG and SLD-resolution do not. Michael Kifer, Eliezer L. Lozinskii |
ICDE | 1 |
| 1987 | A theory of intersection anomalies in relational database schemesabstractThe desirability of acyclic database schemes is well argued in [8] and [13]. For schemas described by multivalued dependencies, acyclicity means that the dependencies do not split each other's left-hand sides and do not form intersection anomalies. In a recent work [4] it is argued that real-world database schemes always meet the former requirement, and in [5] it is shown that any given real-world scheme can be made to satisfy also the latter requirement, after being properly extended. However, the method of elimination of intersection anomalies proposed in [5] is intrinsically nondeterministic—an undesirable property for a design tool. In the present work it is shown that this nondeterminism does not, however, affect the final result of the design process. In addition, we present an efficient deterministic algorithm, which is equivalent to the nondeterministic process of [5]. Along the way a study of intersection anomalies, which is interesting in its own right, is performed. Catriel Beeri, Michael Kifer |
J. ACM | 2 |
| 1986 | Filtering Data Flow in Deductive Databases
Michael Kifer, Eliezer L. Lozinskii |
ICDT | 1 |
| 1986 | Elimination of intersection anomalies from database schemesabstractThe desirability of acyclic (conflict-free) schemes is well argued in [8] and [13]. When a scheme is described by multivalued dependencies, acyclicity means that the dependencies do not split each other's left-hand side and do not form intersection anomalies . It is shown that if the second condition fails to hold, the scheme can be amended so that it does hold. The basic step is to add one attribute and some dependencies to resolve one intersection anomaly. This step generates an extension of the given scheme in which the anomaly does not exist. Also, the iterative use of the basic step is analyzed and it is proved that the transformation so defined terminates and removes all intersection anomalies. Catriel Beeri, Michael Kifer |
J. ACM | 2 |
| 1986 | An Integrated Approach to Logical Design of Relational Database SchemesabstractWe propose a new approach to the design of relational database schemes. The main features of the approach are the following: A combination of the traditional decomposition and synthesis approaches, thus allowing the use of both functional and multivalued dependencies. Separation of structural dependencies relevant for the design process from integrity constraints, that is, constraints that do not bear any structural information about the data and which should therefore be discarded at the design stage. This separation is supported by a simple syntactic test filtering out nonstructural dependencies. Automatic correction of schemes which lack certain desirable properties. Catriel Beeri, Michael Kifer |
ACM Trans. Database Syst. | 2 |
| 1984 | Comprehensive Approach to the Design of Relational Database Schemes
Catriel Beeri, Michael Kifer |
VLDB | 2 |
| 1983 | Elimination of Intersection Anomalies from Database SchemesabstractThe desirability of acyclic database scheme is well argued in [L,BFMY]. When a scheme is described by multivalued dependencies, acyclicity means that the dependencies do not split each other's left-hand side and do not form intersection anomalies. We show that if the second condition fails to hold, the scheme can be amended so that it holds. The basic step is to add one attribute and some dependencies to resolve one intersection anomaly. This step generates an extension of the given scheme in which the anomaly does not exists. We also analyze the repetitive use of the basic step and prove that the transformation so defined removes all intersection anomalies. Finally, we characterize a class of attributes that can be removed from the final scheme, leaving it acyclic. Catriel Beeri, Michael Kifer |
PODS | 2 |