@conference {13075,
	title = {Multi-agent event recognition in structured scenarios},
	booktitle = {Computer Vision and Pattern Recognition (CVPR), 2011 IEEE Conference on},
	year = {2011},
	month = {2011/06//},
	pages = {3289 - 3296},
	abstract = {We present a framework for the automatic recognition of complex multi-agent events in settings where structure is imposed by rules that agents must follow while performing activities. Given semantic spatio-temporal descriptions of what generally happens (i.e., rules, event descriptions, physical constraints), and based on video analysis, we determine the events that occurred. Knowledge about spatio-temporal structure is encoded using first-order logic using an approach based on Allen{\textquoteright}s Interval Logic, and robustness to low-level observation uncertainty is provided by Markov Logic Networks (MLN). Our main contribution is that we integrate interval-based temporal reasoning with probabilistic logical inference, relying on an efficient bottom-up grounding scheme to avoid combinatorial explosion. Applied to one-on-one basketball, our framework detects and tracks players, their hands and feet, and the ball, generates event observations from the resulting trajectories, and performs probabilistic logical inference to determine the most consistent sequence of events. We demonstrate our approach on 1hr (100,000 frames) of outdoor videos.},
	keywords = {Allen, analysis;Markov, descriptions;video, event, grounding, inference;semantic, interval, Logic, logic;interval-based, logic;Markov, logic;multi-agent, logical, networks;bottom-up, processes;formal, processing;, reasoning;multiagent, reasoning;video, recognition;probabilistic, recognition;temporal, scheme;first-order, signal, spatio-temporal, systems;object, temporal},
	doi = {10.1109/CVPR.2011.5995386},
	author = {Morariu,V.I. and Davis, Larry S.}
}
@article {15954,
	title = {Active logic semantics for a single agent in a static world},
	journal = {Artificial Intelligence},
	volume = {172},
	year = {2008},
	month = {2008/05//},
	pages = {1045 - 1063},
	abstract = {For some time we have been developing, and have had significant practical success with, a time-sensitive, contradiction-tolerant logical reasoning engine called the active logic machine (ALMA). The current paper details a semantics for a general version of the underlying logical formalism, active logic. Central to active logic are special rules controlling the inheritance of beliefs in general (and of beliefs about the current time in particular), very tight controls on what can be derived from direct contradictions (P\&{\textlnot}P), and mechanisms allowing an agent to represent and reason about its own beliefs and past reasoning. Furthermore, inspired by the notion that until an agent notices that a set of beliefs is contradictory, that set seems consistent (and the agent therefore reasons with it as if it were consistent), we introduce an "apperception function" that represents an agent{\textquoteright}s limited awareness of its own beliefs, and serves to modify inconsistent belief sets so as to yield consistent sets. Using these ideas, we introduce a new definition of logical consequence in the context of active logic, as well as a new definition of soundness such that, when reasoning with consistent premises, all classically sound rules remain sound in our new sense. However, not everything that is classically sound remains sound in our sense, for by classical definitions, all rules with contradictory premises are vacuously sound, whereas in active logic not everything follows from a contradiction.},
	keywords = {Active logic, Autonomous agents, Brittleness, Logic, Nonmonotonic logic, Paraconsistent logic, semantics, Soundness, TIME},
	isbn = {0004-3702},
	doi = {16/j.artint.2007.11.005},
	url = {http://www.sciencedirect.com/science/article/pii/S0004370207001993},
	author = {Anderson,Michael L. and Gomaa,Walid and Grant,John and Perlis, Don}
}
@conference {13191,
	title = {VidMAP: video monitoring of activity with Prolog},
	booktitle = {Advanced Video and Signal Based Surveillance, 2005. AVSS 2005. IEEE Conference on},
	year = {2005},
	month = {2005/09//},
	pages = {224 - 229},
	abstract = {This paper describes the architecture of a visual surveillance system that combines real time computer vision algorithms with logic programming to represent and recognize activities involving interactions amongst people, packages and the environments through which they move. The low level computer vision algorithms log primitive events of interest as observed facts, while the higher level Prolog based reasoning engine uses these facts in conjunction with predefined rules to recognize various activities in the input video streams. The system is illustrated in action on a multi-camera surveillance scenario that includes both security and safety violations.},
	keywords = {activities, algorithms;, based, Computer, computerised, engine;, higher, image, level, Logic, monitoring;, multicamera, processing;, programming;, Prolog, PROLOG;, reasoning, recognition;, scenario;, signal, streaming;, streams;, Surveillance, surveillance;, system;, video, VISION, vision;, visual},
	doi = {10.1109/AVSS.2005.1577271},
	author = {Shet,V. D and Harwood,D. and Davis, Larry S.}
}
@article {17798,
	title = {Optimal models of disjunctive logic programs: semantics, complexity, and computation},
	journal = {Knowledge and Data Engineering, IEEE Transactions on},
	volume = {16},
	year = {2004},
	month = {2004/04//},
	pages = {487 - 503},
	abstract = {Almost all semantics for logic programs with negation identify a set, SEM(P), of models of program P, as the intended semantics of P, and any model M in this class is considered a possible meaning of P with regard to the semantics the user has in mind. Thus, for example, in the case of stable models [M. Gelfond et al., (1988)], choice models [D. Sacca et al., (1990)], answer sets [M. Gelfond et al., (1991)], etc., different possible models correspond to different ways of "completing" the incomplete information in the logic program. However, different end-users may have different ideas on which of these different models in SEM(P) is a reasonable one from their point of view. For instance, given SEM(P), user U<sub>1</sub> may prefer model M<sub>1</sub> isin;SEM(P) to model M<sub>2</sub> isin;SEM(P) based on some evaluation criterion that she has. We develop a logic program semantics based on optimal models. This semantics does not add yet another semantics to the logic programming arena - it takes as input an existing semantics SEM(P) and a user-specified objective function Obj, and yields a new semantics Opt(P)_ sube; SEM(P) that realizes the objective function within the framework of preferred models identified already by SEM(P). Thus, the user who may or may not know anything about logic programming has considerable flexibility in making the system reflect her own objectives by building "on top" of existing semantics known to the system. In addition to the declarative semantics, we provide a complete complexity analysis and algorithms to compute optimal models under varied conditions when SEM(P) is the stable model semantics, the minimal models semantics, and the all-models semantics.},
	keywords = {complexity;, computational, disjunctive, function;, knowledge, LANGUAGE, Logic, minimal, model, nonmonotonic, objective, optimisation;, OPTIMIZATION, problems;, program, Programming, programming;, reasoning;, representation;, semantics;, stable, user-specified},
	isbn = {1041-4347},
	doi = {10.1109/TKDE.2004.1269672},
	author = {Leone,N. and Scarcello,F. and V.S. Subrahmanian}
}
@article {18892,
	title = {A General Approach to Synthesize Problem-Specific Planners},
	year = {2003},
	month = {2003/10/27/},
	institution = {Department of Computer Science, University of Maryland, College Park},
	abstract = {In this paper, we describe a way to improve the performance of hand-tailorable planners by compiling each domain description into a separate domain-specific planner. We discuss why and when this approach can be useful, and we present experimental results showing that our approach produces significant increases in the speed of planning.},
	keywords = {*PLANNING, *SOFTWARE ENGINEERING, Artificial intelligence, COMPUTER PROGRAMMING AND SOFTWARE, COMPUTER PROGRAMS, Logic, problem solving},
	url = {http://stinet.dtic.mil/oai/oai?\&verb=getRecord\&metadataPrefix=html\&identifier=ADA455023},
	author = {Ilghami,Okhtay and Nau, Dana S.}
}
@article {16479,
	title = {Logic-based query optimization for object databases},
	journal = {IEEE Transactions on Knowledge and Data Engineering},
	volume = {12},
	year = {2000},
	month = {2000/08//Jul},
	pages = {529 - 547},
	abstract = {We present a technique for transferring query optimization techniques, developed for relational databases, into object databases. We demonstrate this technique for ODMG database schemas defined in ODL and object queries expressed in OQL. The object schema is represented using a logical representation (Datalog). Semantic knowledge about the object data model, e.g., class hierarchy information, relationship between objects, etc., as well as semantic knowledge about a particular schema and application domain are expressed as integrity constraints. An OQL object query is represented as a logic query and query optimization is performed in the Datalog representation. We obtain equivalent (optimized) logic queries, and subsequently obtain equivalent (optimized) OQL queries for each equivalent logic query. We present one optimization technique for semantic query optimization (SQO) based on the residue technique of U. Charavarthy et al. (1990; 1986; 1988). We show that our technique generalizes previous research on SQO for object databases. We handle a large class of OQL queries, including queries with constructors and methods. We demonstrate how SQO can be used to eliminate queries which contain contradictions and simplify queries, e.g., by eliminating joins, or by reducing the access scope for evaluating a query to some specific subclass(es). We also demonstrate how the definition of a method or integrity constraints describing the method, can be used in optimizing a query with a method},
	keywords = {access scope, application domain, class hierarchy information, Constraint optimization, data integrity, Data models, Datalog, Datalog representation, deductive databases, equivalent logic query, integrity constraints, Lifting equipment, Logic, logic based query optimization, logic programming, logic queries, logic query, logical representation, object data model, object databases, object queries, object schema, object-oriented databases, ODL, ODMG database schemas, optimization technique, optimized OQL queries, OQL object query, query languages, Query optimization, query optimization techniques, Query processing, Relational databases, residue technique, semantic knowledge, semantic query optimization},
	isbn = {1041-4347},
	doi = {10.1109/69.868906},
	author = {Grant,J. and Gryz,J. and Minker, Jack and Raschid, Louiqa}
}
@conference {15524,
	title = {Semantic query optimization for object databases},
	booktitle = {Data Engineering, 1997. Proceedings. 13th International Conference on},
	year = {1997},
	month = {1997/04//},
	pages = {444 - 453},
	abstract = {Presents a technique for semantic query optimization (SQO) for object databases. We use the ODMG-93 (Object Data Management Group) standard ODL (Object Database Language) and OQL (Object Query Language) languages. The ODL object schema and the OQL object query are translated into a DATALOG representation. Semantic knowledge about the object model and the particular application is expressed as integrity constraints. This is an extension of the ODMG-93 standard. SQO is performed in the DATALOG representation, and an equivalent logic query and (subsequently) an equivalent OQL object query are obtained. SQO is based on the residue technique of Chakravarthy et al. (1990). We show that our technique generalizes previous research on SQO for object databases. It can be applied to queries with structure constructors and method application. It utilizes integrity constraints about keys, methods and knowledge of access support relations, to produce equivalent queries, which may have more efficient evaluation plans},
	keywords = {application;object, constraints;keys;method, constructors;DATALOG;data, databases;object-oriented, databases;query, Datalog, Evaluation, integrity;data, languages;query, Logic, object, optimization;structure, plans;residue, processing;software, query, query;access, query;integrity, relations;equivalent, representation;ODL, schema;ODMG-93, standard;OQL, standards;, structures;object-oriented, Support, technique;semantic},
	doi = {10.1109/ICDE.1997.581983},
	author = {Grant,J. and Gryz,J. and Minker, Jack and Raschid, Louiqa}
}
@conference {12799,
	title = {Efficient model checking via the equational μ-calculus},
	booktitle = {, Eleventh Annual IEEE Symposium on Logic in Computer Science, 1996. LICS {\textquoteright}96. Proceedings},
	year = {1996},
	month = {1996/07/27/30},
	pages = {304 - 312},
	publisher = {IEEE},
	organization = {IEEE},
	abstract = {This paper studies the use of an equational variant of the modal μ-calculus as a unified framework for efficient temporal logic model checking. In particular we show how an expressive temporal logic, CTL*, may be efficiently translated into the μ-calculus. Using this translation, one may then employ μ-calculus model-checking techniques, including on-the-fly procedures, BDD-based algorithms and compositional model-checking approaches, to determine if systems satisfy formulas in CTL*},
	keywords = {Automata, BDD-based algorithms, Boolean functions, Calculus, compositional model-checking approaches, computational complexity, Computer science, CTL*, Data structures, Encoding, equational variant, equational μ-calculus, Equations, expressive temporal logic, Logic, Maintenance, modal μ-calculus, Model checking, on-the-fly procedures, Surges, temporal logic, temporal logic model checking, unified framework},
	isbn = {0-8186-7463-6},
	doi = {10.1109/LICS.1996.561358},
	author = {Bhat,G. and Cleaveland, Rance}
}
@conference {12787,
	title = {Efficient on-the-fly model checking for CTL},
	booktitle = {, Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS {\textquoteright}95. Proceedings},
	year = {1995},
	month = {1995/06/26/29},
	pages = {388 - 397},
	publisher = {IEEE},
	organization = {IEEE},
	abstract = {This paper gives an on-the-fly algorithm for determining whether a finite-state system satisfies a formula in the temporal logic CTL. The time complexity of our algorithm matches that of the best existing {\textquotedblleft}global algorithm{\textquotedblright} for model checking in this logic, and it performs as well as the best known global algorithms for the sublogics CTL and LTL. In contrast with these approaches, however, our routine constructs the state space of the system under consideration in a need-driven fashion and will therefore perform better in practice},
	keywords = {Algorithm design and analysis, Automata, computational complexity, Computer science, CTL, Encoding, finite automata, finite-state system, global algorithm, Logic, LTL, on-the-fly model checking, Performance analysis, Safety, State-space methods, sublogic, temporal logic, time complexity},
	isbn = {0-8186-7050-9},
	doi = {10.1109/LICS.1995.523273},
	author = {Bhat,G. and Cleaveland, Rance and Grumberg,O.}
}
@conference {12783,
	title = {Verifying an intelligent structural control system: a case study},
	booktitle = {Real-Time Systems Symposium, 1994., Proceedings.},
	year = {1994},
	month = {1994/12/07/9},
	pages = {271 - 275},
	publisher = {IEEE},
	organization = {IEEE},
	abstract = {Describes the formal verification of the timing properties of the design of an intelligent structural control system using the Concurrency Workbench, an automatic verification tool for finite-state processes. The high-level design of the system is first given in Modechart, a graphical specification language for real-time systems, and then translated into a temporal process algebra supported by the Workbench. The facilities provided by this tool are then used to analyze the system and ultimately show it to be correct},
	keywords = {automatic verification tool, case study, Concurrency Workbench, Distributed computing, Distributed control, distributed processing, finite automata, finite-state processes, formal verification, graphical specification language, high-level design, intelligent control, intelligent structural control system verification, Logic, Modechart, Process algebra, Real time systems, real-time systems, Specification languages, structural engineering computing, temporal logic, temporal process algebra, time-varying systems, Timing, timing properties, visual languages},
	isbn = {0-8186-6600-5},
	doi = {10.1109/REAL.1994.342708},
	author = {Elseaidy,W. M and Cleaveland, Rance and Baugh,J. W.}
}
