 Extensive research and numerous publications over the past 50 years have developed a variety of logical deduction systems and decision methods for the temporal logics mentioned here and many more. Hilbert style axiomatic systems are the most common logical deduction systems for temporal logics, but many complete systems of semantic tableaux, sequent calculi, and resolution-based systems have been proposed as well. Some general references on deductive systems for temporal logics (in addition to the more specific references mentioned elsewhere in this text) include: Rescher and Urquhart (1971); McArthur (1976); Burgess (1984); Emerson (1990); Goldblatt (1992); Gabbay et al. (1994); van Benthem (1995); Bolc and Szalas (1995); Gabbay and Guenthner (2002); Gabbay et al. (2003); Fisher et al. (2005); Blackburn et al. (2006); Baier and Katoen (2008); Kröger and Merz (2008); Fisher (2011); Demri et al. (2016).